Theorem simpl23 1272

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  frrlem10  8298  mulgdirlem  19234  nosupbnd2lem1  27959  noinfbnd2lem1  27974  brbtwn2  29370  ax5seglem3a  29395  ax5seg  29403  axpasch  29406  axeuclid  29428  br8d  33089  br8  36343  cgrextend  36596  segconeq  36598  segconeu  36599  trisegint  36616  ifscgr  36632  cgrsub  36633  cgrxfr  36643  lineext  36664  seglecgr12im  36698  segletr  36702  lineunray  36735  lineelsb2  36736  cvrcmp  40164  cvlsupr2  40224  atcvrj2b  40313  atexchcvrN  40321  3atlem3  40366  3atlem5  40368  lplnnle2at  40422  lplnllnneN  40437  4atlem3  40477  4atlem10b  40486  4atlem12  40493  2llnma3r  40669  paddasslem4  40704  paddasslem7  40707  paddasslem8  40708  paddasslem12  40712  paddasslem13  40713  paddasslem15  40715  pmodlem1  40727  pmodlem2  40728  atmod1i1m  40739  llnexchb2lem  40749  4atex2  40958  ltrnatlw  41064  arglem1N  41071  cdlemd4  41082  cdlemd5  41083  cdleme16  41166  cdleme20  41205  cdleme21k  41219  cdleme27N  41250  cdleme28c  41253  cdleme43fsv1snlem  41301  cdleme38n  41345  cdleme40n  41349  cdleme41snaw  41357  cdlemg6c  41501  cdlemg8c  41510  cdlemg8  41512  cdlemg12e  41528  cdlemg16ALTN  41539  cdlemg16zz  41541  cdlemg18a  41559  cdlemg20  41566  cdlemg22  41568  cdlemg37  41570  cdlemg31d  41581  cdlemg33  41592  cdlemg38  41596  cdlemg44b  41613  cdlemk33N  41790  cdlemk34  41791  cdlemk38  41796  cdlemk35s-id  41819  cdlemk39s-id  41821  cdlemk53b  41837  cdlemk53  41838  cdlemk55  41842  cdlemk35u  41845  cdlemk55u  41847  cdleml3N  41859  cdlemn11pre  42091  aks6d1c1  42990