Theorem simpl11 1285

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

Assertion

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

Proof of Theorem simpl11

Step	Hyp	Ref	Expression
1		simp11 1222	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜑)
2	1	adantr 472	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072

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 385  df-3an 1074

This theorem is referenced by:  pythagtriplem4  15647  tsmsxp  22080  brbtwn2  25905  ax5seg  25938  3vfriswmgr  27353  br8  31874  nolt02o  32072  btwndiff  32361  ifscgr  32378  seglecgr12im  32444  lkrshp  34812  cvlcvr1  35046  atbtwn  35152  3dimlem3  35167  3dimlem3OLDN  35168  1cvratex  35179  llnmlplnN  35245  4atlem3  35302  4atlem3a  35303  4atlem11  35315  4atlem12  35318  lnatexN  35485  cdlemb  35500  paddasslem4  35529  paddasslem10  35535  pmodlem1  35552  llnexchb2lem  35574  llnexchb2  35575  arglem1N  35897  cdlemd4  35908  cdlemd9  35913  cdlemd  35914  cdleme16  35992  cdleme20  36031  cdleme21i  36042  cdleme21k  36045  cdleme27N  36076  cdleme28c  36079  cdlemefrs29bpre0  36103  cdlemefrs29clN  36106  cdlemefrs32fva  36107  cdleme41sn3a  36140  cdleme32fva  36144  cdleme40n  36175  cdlemg12e  36354  cdlemg15a  36362  cdlemg15  36363  cdlemg16ALTN  36365  cdlemg16z  36366  cdlemg20  36392  cdlemg22  36394  cdlemg29  36412  cdlemg38  36422  cdlemk33N  36616  cdlemk56  36678  dihord11b  36930  dihord2pre  36933  dihord4  36966  fourierdlem77  40820