Theorem simpl12 1249

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

Assertion

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

Proof of Theorem simpl12

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  pythagtriplem4  16702  pmatcollpw1lem1  22160  pmatcollpw1  22162  mp2pm2mplem2  22193  nolt02o  27080  nogt01o  27081  brbtwn2  27917  ax5seg  27950  3vfriswmgr  29285  br8  34415  ifscgr  34705  seglecgr12im  34771  lkrshp  37640  atlatle  37855  cvlcvr1  37874  atbtwn  37982  3dimlem3  37997  3dimlem3OLDN  37998  1cvratex  38009  llnmlplnN  38075  4atlem3  38132  4atlem3a  38133  4atlem11  38145  4atlem12  38148  cdlemb  38330  paddasslem4  38359  paddasslem10  38365  pmodlem1  38382  llnexchb2lem  38404  arglem1N  38726  cdlemd4  38737  cdlemd  38743  cdleme16  38821  cdleme20  38860  cdleme21k  38874  cdleme22cN  38878  cdleme27N  38905  cdleme28c  38908  cdleme29ex  38910  cdleme32fva  38973  cdleme40n  39004  cdlemg15a  39191  cdlemg15  39192  cdlemg16ALTN  39194  cdlemg16z  39195  cdlemg20  39221  cdlemg22  39223  cdlemg29  39241  cdlemg38  39251  cdlemk33N  39445  cdlemk56  39507  fourierdlem77  44544