Theorem simpl13 1138

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simpl13	⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜒)

Proof of Theorem simpl13

Step	Hyp	Ref	Expression
1		simp13 1093	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜒)
2	1	adantr 481	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  pythagtriplem4  15524  mply1topmatcl  20610  brbtwn2  25785  ax5seg  25818  br8  31646  nolt02o  31845  btwndiff  32134  ifscgr  32151  seglecgr12im  32217  atlatle  34607  cvlcvr1  34626  atbtwn  34732  3dimlem3  34747  3dimlem3OLDN  34748  4atlem3  34882  4atlem11  34895  4atlem12  34898  2lplnj  34906  paddasslem4  35109  paddasslem10  35115  pmodlem1  35132  llnexchb2lem  35154  pclfinclN  35236  arglem1N  35477  cdlemd4  35488  cdlemd  35494  cdleme16  35572  cdleme20  35612  cdleme21k  35626  cdleme22cN  35630  cdleme27N  35657  cdleme28c  35660  cdleme29ex  35662  cdleme32fva  35725  cdleme40n  35756  cdlemg15a  35943  cdlemg15  35944  cdlemg16ALTN  35946  cdlemg16z  35947  cdlemg20  35973  cdlemg22  35975  cdlemg29  35993  cdlemg38  36003  cdlemk56  36259  dihord2pre  36514  uzwo4  39221  fourierdlem77  40400