Theorem simpl23 1255

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  frrlem10  8238  mulgdirlem  19072  nosupbnd2lem1  27693  noinfbnd2lem1  27708  brbtwn2  28988  ax5seglem3a  29013  ax5seg  29021  axpasch  29024  axeuclid  29046  br8d  32696  br8  35954  cgrextend  36206  segconeq  36208  segconeu  36209  trisegint  36226  ifscgr  36242  cgrsub  36243  cgrxfr  36253  lineext  36274  seglecgr12im  36308  segletr  36312  lineunray  36345  lineelsb2  36346  cvrcmp  39743  cvlsupr2  39803  atcvrj2b  39892  atexchcvrN  39900  3atlem3  39945  3atlem5  39947  lplnnle2at  40001  lplnllnneN  40016  4atlem3  40056  4atlem10b  40065  4atlem12  40072  2llnma3r  40248  paddasslem4  40283  paddasslem7  40286  paddasslem8  40287  paddasslem12  40291  paddasslem13  40292  paddasslem15  40294  pmodlem1  40306  pmodlem2  40307  atmod1i1m  40318  llnexchb2lem  40328  4atex2  40537  ltrnatlw  40643  arglem1N  40650  cdlemd4  40661  cdlemd5  40662  cdleme16  40745  cdleme20  40784  cdleme21k  40798  cdleme27N  40829  cdleme28c  40832  cdleme43fsv1snlem  40880  cdleme38n  40924  cdleme40n  40928  cdleme41snaw  40936  cdlemg6c  41080  cdlemg8c  41089  cdlemg8  41091  cdlemg12e  41107  cdlemg16ALTN  41118  cdlemg16zz  41120  cdlemg18a  41138  cdlemg20  41145  cdlemg22  41147  cdlemg37  41149  cdlemg31d  41160  cdlemg33  41171  cdlemg38  41175  cdlemg44b  41192  cdlemk33N  41369  cdlemk34  41370  cdlemk38  41375  cdlemk35s-id  41398  cdlemk39s-id  41400  cdlemk53b  41416  cdlemk53  41417  cdlemk55  41421  cdlemk35u  41424  cdlemk55u  41426  cdleml3N  41438  cdlemn11pre  41670  aks6d1c1  42569