Theorem simpl23 1253

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 1193	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜒)
2	1	3ad2antl2 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:  frrlem10  8336  mulgdirlem  19145  nosupbnd2lem1  27778  noinfbnd2lem1  27793  brbtwn2  28938  ax5seglem3a  28963  ax5seg  28971  axpasch  28974  axeuclid  28996  br8d  32632  br8  35718  cgrextend  35972  segconeq  35974  segconeu  35975  trisegint  35992  ifscgr  36008  cgrsub  36009  cgrxfr  36019  lineext  36040  seglecgr12im  36074  segletr  36078  lineunray  36111  lineelsb2  36112  cvrcmp  39239  cvlsupr2  39299  atcvrj2b  39389  atexchcvrN  39397  3atlem3  39442  3atlem5  39444  lplnnle2at  39498  lplnllnneN  39513  4atlem3  39553  4atlem10b  39562  4atlem12  39569  2llnma3r  39745  paddasslem4  39780  paddasslem7  39783  paddasslem8  39784  paddasslem12  39788  paddasslem13  39789  paddasslem15  39791  pmodlem1  39803  pmodlem2  39804  atmod1i1m  39815  llnexchb2lem  39825  4atex2  40034  ltrnatlw  40140  arglem1N  40147  cdlemd4  40158  cdlemd5  40159  cdleme16  40242  cdleme20  40281  cdleme21k  40295  cdleme27N  40326  cdleme28c  40329  cdleme43fsv1snlem  40377  cdleme38n  40421  cdleme40n  40425  cdleme41snaw  40433  cdlemg6c  40577  cdlemg8c  40586  cdlemg8  40588  cdlemg12e  40604  cdlemg16ALTN  40615  cdlemg16zz  40617  cdlemg18a  40635  cdlemg20  40642  cdlemg22  40644  cdlemg37  40646  cdlemg31d  40657  cdlemg33  40668  cdlemg38  40672  cdlemg44b  40689  cdlemk33N  40866  cdlemk34  40867  cdlemk38  40872  cdlemk35s-id  40895  cdlemk39s-id  40897  cdlemk53b  40913  cdlemk53  40914  cdlemk55  40918  cdlemk35u  40921  cdlemk55u  40923  cdleml3N  40935  cdlemn11pre  41167  aks6d1c1  42073