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 397   ∧ 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 206  df-an 398  df-3an 1089

This theorem is referenced by:  frrlem10  8142  mulgdirlem  18779  brbtwn2  27318  ax5seglem3a  27343  ax5seg  27351  axpasch  27354  axeuclid  27376  br8d  30995  br8  33768  nosupbnd2lem1  33963  noinfbnd2lem1  33978  cgrextend  34355  segconeq  34357  segconeu  34358  trisegint  34375  ifscgr  34391  cgrsub  34392  cgrxfr  34402  lineext  34423  seglecgr12im  34457  segletr  34461  lineunray  34494  lineelsb2  34495  cvrcmp  37339  cvlsupr2  37399  atcvrj2b  37488  atexchcvrN  37496  3atlem3  37541  3atlem5  37543  lplnnle2at  37597  lplnllnneN  37612  4atlem3  37652  4atlem10b  37661  4atlem12  37668  2llnma3r  37844  paddasslem4  37879  paddasslem7  37882  paddasslem8  37883  paddasslem12  37887  paddasslem13  37888  paddasslem15  37890  pmodlem1  37902  pmodlem2  37903  atmod1i1m  37914  llnexchb2lem  37924  4atex2  38133  ltrnatlw  38239  arglem1N  38246  cdlemd4  38257  cdlemd5  38258  cdleme16  38341  cdleme20  38380  cdleme21k  38394  cdleme27N  38425  cdleme28c  38428  cdleme43fsv1snlem  38476  cdleme38n  38520  cdleme40n  38524  cdleme41snaw  38532  cdlemg6c  38676  cdlemg8c  38685  cdlemg8  38687  cdlemg12e  38703  cdlemg16ALTN  38714  cdlemg16zz  38716  cdlemg18a  38734  cdlemg20  38741  cdlemg22  38743  cdlemg37  38745  cdlemg31d  38756  cdlemg33  38767  cdlemg38  38771  cdlemg44b  38788  cdlemk33N  38965  cdlemk34  38966  cdlemk38  38971  cdlemk35s-id  38994  cdlemk39s-id  38996  cdlemk53b  39012  cdlemk53  39013  cdlemk55  39017  cdlemk35u  39020  cdlemk55u  39022  cdleml3N  39034  cdlemn11pre  39266