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  8274  mulgdirlem  19037  nosupbnd2lem1  27627  noinfbnd2lem1  27642  brbtwn2  28832  ax5seglem3a  28857  ax5seg  28865  axpasch  28868  axeuclid  28890  br8d  32538  br8  35743  cgrextend  35996  segconeq  35998  segconeu  35999  trisegint  36016  ifscgr  36032  cgrsub  36033  cgrxfr  36043  lineext  36064  seglecgr12im  36098  segletr  36102  lineunray  36135  lineelsb2  36136  cvrcmp  39276  cvlsupr2  39336  atcvrj2b  39426  atexchcvrN  39434  3atlem3  39479  3atlem5  39481  lplnnle2at  39535  lplnllnneN  39550  4atlem3  39590  4atlem10b  39599  4atlem12  39606  2llnma3r  39782  paddasslem4  39817  paddasslem7  39820  paddasslem8  39821  paddasslem12  39825  paddasslem13  39826  paddasslem15  39828  pmodlem1  39840  pmodlem2  39841  atmod1i1m  39852  llnexchb2lem  39862  4atex2  40071  ltrnatlw  40177  arglem1N  40184  cdlemd4  40195  cdlemd5  40196  cdleme16  40279  cdleme20  40318  cdleme21k  40332  cdleme27N  40363  cdleme28c  40366  cdleme43fsv1snlem  40414  cdleme38n  40458  cdleme40n  40462  cdleme41snaw  40470  cdlemg6c  40614  cdlemg8c  40623  cdlemg8  40625  cdlemg12e  40641  cdlemg16ALTN  40652  cdlemg16zz  40654  cdlemg18a  40672  cdlemg20  40679  cdlemg22  40681  cdlemg37  40683  cdlemg31d  40694  cdlemg33  40705  cdlemg38  40709  cdlemg44b  40726  cdlemk33N  40903  cdlemk34  40904  cdlemk38  40909  cdlemk35s-id  40932  cdlemk39s-id  40934  cdlemk53b  40950  cdlemk53  40951  cdlemk55  40955  cdlemk35u  40958  cdlemk55u  40960  cdleml3N  40972  cdlemn11pre  41204  aks6d1c1  42104