Theorem simpl23 1252

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 1192	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜒)
2	1	3ad2antl2 1185	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  8319  mulgdirlem  19136  nosupbnd2lem1  27775  noinfbnd2lem1  27790  brbtwn2  28935  ax5seglem3a  28960  ax5seg  28968  axpasch  28971  axeuclid  28993  br8d  32630  br8  35736  cgrextend  35990  segconeq  35992  segconeu  35993  trisegint  36010  ifscgr  36026  cgrsub  36027  cgrxfr  36037  lineext  36058  seglecgr12im  36092  segletr  36096  lineunray  36129  lineelsb2  36130  cvrcmp  39265  cvlsupr2  39325  atcvrj2b  39415  atexchcvrN  39423  3atlem3  39468  3atlem5  39470  lplnnle2at  39524  lplnllnneN  39539  4atlem3  39579  4atlem10b  39588  4atlem12  39595  2llnma3r  39771  paddasslem4  39806  paddasslem7  39809  paddasslem8  39810  paddasslem12  39814  paddasslem13  39815  paddasslem15  39817  pmodlem1  39829  pmodlem2  39830  atmod1i1m  39841  llnexchb2lem  39851  4atex2  40060  ltrnatlw  40166  arglem1N  40173  cdlemd4  40184  cdlemd5  40185  cdleme16  40268  cdleme20  40307  cdleme21k  40321  cdleme27N  40352  cdleme28c  40355  cdleme43fsv1snlem  40403  cdleme38n  40447  cdleme40n  40451  cdleme41snaw  40459  cdlemg6c  40603  cdlemg8c  40612  cdlemg8  40614  cdlemg12e  40630  cdlemg16ALTN  40641  cdlemg16zz  40643  cdlemg18a  40661  cdlemg20  40668  cdlemg22  40670  cdlemg37  40672  cdlemg31d  40683  cdlemg33  40694  cdlemg38  40698  cdlemg44b  40715  cdlemk33N  40892  cdlemk34  40893  cdlemk38  40898  cdlemk35s-id  40921  cdlemk39s-id  40923  cdlemk53b  40939  cdlemk53  40940  cdlemk55  40944  cdlemk35u  40947  cdlemk55u  40949  cdleml3N  40961  cdlemn11pre  41193  aks6d1c1  42098