Theorem simpl23 1254

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 1194	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜒)
2	1	3ad2antl2 1187	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜒)

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

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 1088

This theorem is referenced by:  frrlem10  8225  mulgdirlem  19015  nosupbnd2lem1  27652  noinfbnd2lem1  27667  brbtwn2  28881  ax5seglem3a  28906  ax5seg  28914  axpasch  28917  axeuclid  28939  br8d  32586  br8  35788  cgrextend  36041  segconeq  36043  segconeu  36044  trisegint  36061  ifscgr  36077  cgrsub  36078  cgrxfr  36088  lineext  36109  seglecgr12im  36143  segletr  36147  lineunray  36180  lineelsb2  36181  cvrcmp  39321  cvlsupr2  39381  atcvrj2b  39470  atexchcvrN  39478  3atlem3  39523  3atlem5  39525  lplnnle2at  39579  lplnllnneN  39594  4atlem3  39634  4atlem10b  39643  4atlem12  39650  2llnma3r  39826  paddasslem4  39861  paddasslem7  39864  paddasslem8  39865  paddasslem12  39869  paddasslem13  39870  paddasslem15  39872  pmodlem1  39884  pmodlem2  39885  atmod1i1m  39896  llnexchb2lem  39906  4atex2  40115  ltrnatlw  40221  arglem1N  40228  cdlemd4  40239  cdlemd5  40240  cdleme16  40323  cdleme20  40362  cdleme21k  40376  cdleme27N  40407  cdleme28c  40410  cdleme43fsv1snlem  40458  cdleme38n  40502  cdleme40n  40506  cdleme41snaw  40514  cdlemg6c  40658  cdlemg8c  40667  cdlemg8  40669  cdlemg12e  40685  cdlemg16ALTN  40696  cdlemg16zz  40698  cdlemg18a  40716  cdlemg20  40723  cdlemg22  40725  cdlemg37  40727  cdlemg31d  40738  cdlemg33  40749  cdlemg38  40753  cdlemg44b  40770  cdlemk33N  40947  cdlemk34  40948  cdlemk38  40953  cdlemk35s-id  40976  cdlemk39s-id  40978  cdlemk53b  40994  cdlemk53  40995  cdlemk55  40999  cdlemk35u  41002  cdlemk55u  41004  cdleml3N  41016  cdlemn11pre  41248  aks6d1c1  42148