Theorem simpl13 1269

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

Assertion

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

Proof of Theorem simpl13

Step	Hyp	Ref	Expression
1		simpl3 1212	. 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  17003  mply1topmatcl  23129  nolt02o  28058  nogt01o  28059  cofslts  28310  coinitslts  28311  brbtwn2  29489  ax5seg  29522  br8  36614  btwndiff  36885  ifscgr  36902  seglecgr12im  36968  atlatle  40471  cvlcvr1  40490  atbtwn  40597  3dimlem3  40612  3dimlem3OLDN  40613  4atlem3  40747  4atlem11  40760  4atlem12  40763  2lplnj  40771  paddasslem4  40974  paddasslem10  40980  pmodlem1  40997  llnexchb2lem  41019  pclfinclN  41101  arglem1N  41341  cdlemd4  41352  cdlemd  41358  cdleme16  41436  cdleme20  41475  cdleme21k  41489  cdleme22cN  41493  cdleme27N  41520  cdleme28c  41523  cdleme29ex  41525  cdleme32fva  41588  cdleme40n  41619  cdlemg15a  41806  cdlemg15  41807  cdlemg16ALTN  41809  cdlemg16z  41810  cdlemg20  41836  cdlemg22  41838  cdlemg29  41856  cdlemg38  41866  cdlemk56  42122  dihord2pre  42376  ismnu  45339  uzwo4  46164  fourierdlem77  47287