Theorem simpl23 1251

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

Assertion

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

Proof of Theorem simpl23

Step	Hyp	Ref	Expression
1		simpl3 1191	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜒)
2	1	3ad2antl2 1184	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  frrlem10  8294  mulgdirlem  19053  nosupbnd2lem1  27641  noinfbnd2lem1  27656  brbtwn2  28709  ax5seglem3a  28734  ax5seg  28742  axpasch  28745  axeuclid  28767  br8d  32393  br8  35340  cgrextend  35594  segconeq  35596  segconeu  35597  trisegint  35614  ifscgr  35630  cgrsub  35631  cgrxfr  35641  lineext  35662  seglecgr12im  35696  segletr  35700  lineunray  35733  lineelsb2  35734  cvrcmp  38744  cvlsupr2  38804  atcvrj2b  38894  atexchcvrN  38902  3atlem3  38947  3atlem5  38949  lplnnle2at  39003  lplnllnneN  39018  4atlem3  39058  4atlem10b  39067  4atlem12  39074  2llnma3r  39250  paddasslem4  39285  paddasslem7  39288  paddasslem8  39289  paddasslem12  39293  paddasslem13  39294  paddasslem15  39296  pmodlem1  39308  pmodlem2  39309  atmod1i1m  39320  llnexchb2lem  39330  4atex2  39539  ltrnatlw  39645  arglem1N  39652  cdlemd4  39663  cdlemd5  39664  cdleme16  39747  cdleme20  39786  cdleme21k  39800  cdleme27N  39831  cdleme28c  39834  cdleme43fsv1snlem  39882  cdleme38n  39926  cdleme40n  39930  cdleme41snaw  39938  cdlemg6c  40082  cdlemg8c  40091  cdlemg8  40093  cdlemg12e  40109  cdlemg16ALTN  40120  cdlemg16zz  40122  cdlemg18a  40140  cdlemg20  40147  cdlemg22  40149  cdlemg37  40151  cdlemg31d  40162  cdlemg33  40173  cdlemg38  40177  cdlemg44b  40194  cdlemk33N  40371  cdlemk34  40372  cdlemk38  40377  cdlemk35s-id  40400  cdlemk39s-id  40402  cdlemk53b  40418  cdlemk53  40419  cdlemk55  40423  cdlemk35u  40426  cdlemk55u  40428  cdleml3N  40440  cdlemn11pre  40672  aks6d1c1  41572