Theorem simpl11 1248

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)

Assertion

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

Proof of Theorem simpl11

Step	Hyp	Ref	Expression
1		simpl1 1191	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜑)
2	1	3ad2antl1 1185	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  pythagtriplem4  16866  tsmsxp  24184  nolt02o  27758  nogt01o  27759  cofsslt  27970  brbtwn2  28938  ax5seg  28971  3vfriswmgr  30310  br8  35718  btwndiff  35991  ifscgr  36008  seglecgr12im  36074  lkrshp  39061  cvlcvr1  39295  atbtwn  39403  3dimlem3  39418  3dimlem3OLDN  39419  1cvratex  39430  llnmlplnN  39496  4atlem3  39553  4atlem3a  39554  4atlem11  39566  4atlem12  39569  lnatexN  39736  cdlemb  39751  paddasslem4  39780  paddasslem10  39786  pmodlem1  39803  llnexchb2lem  39825  llnexchb2  39826  arglem1N  40147  cdlemd4  40158  cdlemd9  40163  cdlemd  40164  cdleme16  40242  cdleme20  40281  cdleme21i  40292  cdleme21k  40295  cdleme27N  40326  cdleme28c  40329  cdlemefrs29bpre0  40353  cdlemefrs29clN  40356  cdlemefrs32fva  40357  cdleme41sn3a  40390  cdleme32fva  40394  cdleme40n  40425  cdlemg12e  40604  cdlemg15a  40612  cdlemg15  40613  cdlemg16ALTN  40615  cdlemg16z  40616  cdlemg20  40642  cdlemg22  40644  cdlemg29  40662  cdlemg38  40672  cdlemk33N  40866  cdlemk56  40928  dihord11b  41179  dihord2pre  41182  dihord4  41215  ismnu  44230  fourierdlem77  46104