Theorem simpl12 1268

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 1211	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜓)
2	1	3ad2antl1 1204	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  pythagtriplem4  16977  pmatcollpw1lem1  23072  pmatcollpw1  23074  mp2pm2mplem2  23105  nolt02o  28034  nogt01o  28035  brbtwn2  29465  ax5seg  29498  3vfriswmgr  30861  br8  36490  ifscgr  36779  seglecgr12im  36845  lkrshp  40130  atlatle  40345  cvlcvr1  40364  atbtwn  40471  3dimlem3  40486  3dimlem3OLDN  40487  1cvratex  40498  llnmlplnN  40564  4atlem3  40621  4atlem3a  40622  4atlem11  40634  4atlem12  40637  cdlemb  40819  paddasslem4  40848  paddasslem10  40854  pmodlem1  40871  llnexchb2lem  40893  arglem1N  41215  cdlemd4  41226  cdlemd  41232  cdleme16  41310  cdleme20  41349  cdleme21k  41363  cdleme22cN  41367  cdleme27N  41394  cdleme28c  41397  cdleme29ex  41399  cdleme32fva  41462  cdleme40n  41493  cdlemg15a  41680  cdlemg15  41681  cdlemg16ALTN  41683  cdlemg16z  41684  cdlemg20  41710  cdlemg22  41712  cdlemg29  41730  cdlemg38  41740  cdlemk33N  41934  cdlemk56  41996  fourierdlem77  47137