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  8301  mulgdirlem  19202  nosupbnd2lem1  27916  noinfbnd2lem1  27931  brbtwn2  29292  ax5seglem3a  29317  ax5seg  29325  axpasch  29328  axeuclid  29350  br8d  32990  br8  36269  cgrextend  36521  segconeq  36523  segconeu  36524  trisegint  36541  ifscgr  36557  cgrsub  36558  cgrxfr  36568  lineext  36589  seglecgr12im  36623  segletr  36627  lineunray  36660  lineelsb2  36661  cvrcmp  40098  cvlsupr2  40158  atcvrj2b  40247  atexchcvrN  40255  3atlem3  40300  3atlem5  40302  lplnnle2at  40356  lplnllnneN  40371  4atlem3  40411  4atlem10b  40420  4atlem12  40427  2llnma3r  40603  paddasslem4  40638  paddasslem7  40641  paddasslem8  40642  paddasslem12  40646  paddasslem13  40647  paddasslem15  40649  pmodlem1  40661  pmodlem2  40662  atmod1i1m  40673  llnexchb2lem  40683  4atex2  40892  ltrnatlw  40998  arglem1N  41005  cdlemd4  41016  cdlemd5  41017  cdleme16  41100  cdleme20  41139  cdleme21k  41153  cdleme27N  41184  cdleme28c  41187  cdleme43fsv1snlem  41235  cdleme38n  41279  cdleme40n  41283  cdleme41snaw  41291  cdlemg6c  41435  cdlemg8c  41444  cdlemg8  41446  cdlemg12e  41462  cdlemg16ALTN  41473  cdlemg16zz  41475  cdlemg18a  41493  cdlemg20  41500  cdlemg22  41502  cdlemg37  41504  cdlemg31d  41515  cdlemg33  41526  cdlemg38  41530  cdlemg44b  41547  cdlemk33N  41724  cdlemk34  41725  cdlemk38  41730  cdlemk35s-id  41753  cdlemk39s-id  41755  cdlemk53b  41771  cdlemk53  41772  cdlemk55  41776  cdlemk35u  41779  cdlemk55u  41781  cdleml3N  41793  cdlemn11pre  42025  aks6d1c1  42924