Theorem simpl23 1250

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  mulgdirlem  18250  brbtwn2  26699  ax5seglem3a  26724  ax5seg  26732  axpasch  26735  axeuclid  26757  br8d  30374  br8  33105  frrlem10  33245  nosupbnd2lem1  33328  cgrextend  33582  segconeq  33584  segconeu  33585  trisegint  33602  ifscgr  33618  cgrsub  33619  cgrxfr  33629  lineext  33650  seglecgr12im  33684  segletr  33688  lineunray  33721  lineelsb2  33722  cvrcmp  36579  cvlsupr2  36639  atcvrj2b  36728  atexchcvrN  36736  3atlem3  36781  3atlem5  36783  lplnnle2at  36837  lplnllnneN  36852  4atlem3  36892  4atlem10b  36901  4atlem12  36908  2llnma3r  37084  paddasslem4  37119  paddasslem7  37122  paddasslem8  37123  paddasslem12  37127  paddasslem13  37128  paddasslem15  37130  pmodlem1  37142  pmodlem2  37143  atmod1i1m  37154  llnexchb2lem  37164  4atex2  37373  ltrnatlw  37479  arglem1N  37486  cdlemd4  37497  cdlemd5  37498  cdleme16  37581  cdleme20  37620  cdleme21k  37634  cdleme27N  37665  cdleme28c  37668  cdleme43fsv1snlem  37716  cdleme38n  37760  cdleme40n  37764  cdleme41snaw  37772  cdlemg6c  37916  cdlemg8c  37925  cdlemg8  37927  cdlemg12e  37943  cdlemg16ALTN  37954  cdlemg16zz  37956  cdlemg18a  37974  cdlemg20  37981  cdlemg22  37983  cdlemg37  37985  cdlemg31d  37996  cdlemg33  38007  cdlemg38  38011  cdlemg44b  38028  cdlemk33N  38205  cdlemk34  38206  cdlemk38  38211  cdlemk35s-id  38234  cdlemk39s-id  38236  cdlemk53b  38252  cdlemk53  38253  cdlemk55  38257  cdlemk35u  38260  cdlemk55u  38262  cdleml3N  38274  cdlemn11pre  38506