Theorem simpl13 1251

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 1194	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜒)
2	1	3ad2antl1 1186	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  16857  mply1topmatcl  22811  nolt02o  27740  nogt01o  27741  cofsslt  27952  coinitsslt  27953  brbtwn2  28920  ax5seg  28953  br8  35756  btwndiff  36028  ifscgr  36045  seglecgr12im  36111  atlatle  39321  cvlcvr1  39340  atbtwn  39448  3dimlem3  39463  3dimlem3OLDN  39464  4atlem3  39598  4atlem11  39611  4atlem12  39614  2lplnj  39622  paddasslem4  39825  paddasslem10  39831  pmodlem1  39848  llnexchb2lem  39870  pclfinclN  39952  arglem1N  40192  cdlemd4  40203  cdlemd  40209  cdleme16  40287  cdleme20  40326  cdleme21k  40340  cdleme22cN  40344  cdleme27N  40371  cdleme28c  40374  cdleme29ex  40376  cdleme32fva  40439  cdleme40n  40470  cdlemg15a  40657  cdlemg15  40658  cdlemg16ALTN  40660  cdlemg16z  40661  cdlemg20  40687  cdlemg22  40689  cdlemg29  40707  cdlemg38  40717  cdlemk56  40973  dihord2pre  41227  ismnu  44280  uzwo4  45058  fourierdlem77  46198