Theorem simpl11 1136

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

Assertion

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

Proof of Theorem simpl11

Step	Hyp	Ref	Expression
1		simp11 1091	. 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  tsmsxp  21958  brbtwn2  25785  ax5seg  25818  3vfriswmgr  27142  br8  31646  nolt02o  31845  btwndiff  32134  ifscgr  32151  seglecgr12im  32217  lkrshp  34392  cvlcvr1  34626  atbtwn  34732  3dimlem3  34747  3dimlem3OLDN  34748  1cvratex  34759  llnmlplnN  34825  4atlem3  34882  4atlem3a  34883  4atlem11  34895  4atlem12  34898  lnatexN  35065  cdlemb  35080  paddasslem4  35109  paddasslem10  35115  pmodlem1  35132  llnexchb2lem  35154  llnexchb2  35155  arglem1N  35477  cdlemd4  35488  cdlemd9  35493  cdlemd  35494  cdleme16  35572  cdleme20  35612  cdleme21i  35623  cdleme21k  35626  cdleme27N  35657  cdleme28c  35660  cdlemefrs29bpre0  35684  cdlemefrs29clN  35687  cdlemefrs32fva  35688  cdleme41sn3a  35721  cdleme32fva  35725  cdleme40n  35756  cdlemg12e  35935  cdlemg15a  35943  cdlemg15  35944  cdlemg16ALTN  35946  cdlemg16z  35947  cdlemg20  35973  cdlemg22  35975  cdlemg29  35993  cdlemg38  36003  cdlemk33N  36197  cdlemk56  36259  dihord11b  36511  dihord2pre  36514  dihord4  36547  fourierdlem77  40400