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 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 401  df-3an 1105

This theorem is referenced by:  frrlem10  8293  mulgdirlem  19172  nosupbnd2lem1  27857  noinfbnd2lem1  27872  brbtwn2  29233  ax5seglem3a  29258  ax5seg  29266  axpasch  29269  axeuclid  29291  br8d  32931  br8  36226  cgrextend  36478  segconeq  36480  segconeu  36481  trisegint  36498  ifscgr  36514  cgrsub  36515  cgrxfr  36525  lineext  36546  seglecgr12im  36580  segletr  36584  lineunray  36617  lineelsb2  36618  cvrcmp  40035  cvlsupr2  40095  atcvrj2b  40184  atexchcvrN  40192  3atlem3  40237  3atlem5  40239  lplnnle2at  40293  lplnllnneN  40308  4atlem3  40348  4atlem10b  40357  4atlem12  40364  2llnma3r  40540  paddasslem4  40575  paddasslem7  40578  paddasslem8  40579  paddasslem12  40583  paddasslem13  40584  paddasslem15  40586  pmodlem1  40598  pmodlem2  40599  atmod1i1m  40610  llnexchb2lem  40620  4atex2  40829  ltrnatlw  40935  arglem1N  40942  cdlemd4  40953  cdlemd5  40954  cdleme16  41037  cdleme20  41076  cdleme21k  41090  cdleme27N  41121  cdleme28c  41124  cdleme43fsv1snlem  41172  cdleme38n  41216  cdleme40n  41220  cdleme41snaw  41228  cdlemg6c  41372  cdlemg8c  41381  cdlemg8  41383  cdlemg12e  41399  cdlemg16ALTN  41410  cdlemg16zz  41412  cdlemg18a  41430  cdlemg20  41437  cdlemg22  41439  cdlemg37  41441  cdlemg31d  41452  cdlemg33  41463  cdlemg38  41467  cdlemg44b  41484  cdlemk33N  41661  cdlemk34  41662  cdlemk38  41667  cdlemk35s-id  41690  cdlemk39s-id  41692  cdlemk53b  41708  cdlemk53  41709  cdlemk55  41713  cdlemk35u  41716  cdlemk55u  41718  cdleml3N  41730  cdlemn11pre  41962  aks6d1c1  42861