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  17002  pmatcollpw1lem1  23097  pmatcollpw1  23099  mp2pm2mplem2  23130  nolt02o  28057  nogt01o  28058  brbtwn2  29488  ax5seg  29521  3vfriswmgr  30884  br8  36613  ifscgr  36901  seglecgr12im  36967  lkrshp  40255  atlatle  40470  cvlcvr1  40489  atbtwn  40596  3dimlem3  40611  3dimlem3OLDN  40612  1cvratex  40623  llnmlplnN  40689  4atlem3  40746  4atlem3a  40747  4atlem11  40759  4atlem12  40762  cdlemb  40944  paddasslem4  40973  paddasslem10  40979  pmodlem1  40996  llnexchb2lem  41018  arglem1N  41340  cdlemd4  41351  cdlemd  41357  cdleme16  41435  cdleme20  41474  cdleme21k  41488  cdleme22cN  41492  cdleme27N  41519  cdleme28c  41522  cdleme29ex  41524  cdleme32fva  41587  cdleme40n  41618  cdlemg15a  41805  cdlemg15  41806  cdlemg16ALTN  41808  cdlemg16z  41809  cdlemg20  41835  cdlemg22  41837  cdlemg29  41855  cdlemg38  41865  cdlemk33N  42059  cdlemk56  42121  fourierdlem77  47286