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  8297  mulgdirlem  19295  nosupbnd2lem1  28054  noinfbnd2lem1  28069  brbtwn2  29465  ax5seglem3a  29490  ax5seg  29498  axpasch  29501  axeuclid  29523  br8d  33184  br8  36490  cgrextend  36743  segconeq  36745  segconeu  36746  trisegint  36763  ifscgr  36779  cgrsub  36780  cgrxfr  36790  lineext  36811  seglecgr12im  36845  segletr  36849  lineunray  36882  lineelsb2  36883  cvrcmp  40308  cvlsupr2  40368  atcvrj2b  40457  atexchcvrN  40465  3atlem3  40510  3atlem5  40512  lplnnle2at  40566  lplnllnneN  40581  4atlem3  40621  4atlem10b  40630  4atlem12  40637  2llnma3r  40813  paddasslem4  40848  paddasslem7  40851  paddasslem8  40852  paddasslem12  40856  paddasslem13  40857  paddasslem15  40859  pmodlem1  40871  pmodlem2  40872  atmod1i1m  40883  llnexchb2lem  40893  4atex2  41102  ltrnatlw  41208  arglem1N  41215  cdlemd4  41226  cdlemd5  41227  cdleme16  41310  cdleme20  41349  cdleme21k  41363  cdleme27N  41394  cdleme28c  41397  cdleme43fsv1snlem  41445  cdleme38n  41489  cdleme40n  41493  cdleme41snaw  41501  cdlemg6c  41645  cdlemg8c  41654  cdlemg8  41656  cdlemg12e  41672  cdlemg16ALTN  41683  cdlemg16zz  41685  cdlemg18a  41703  cdlemg20  41710  cdlemg22  41712  cdlemg37  41714  cdlemg31d  41725  cdlemg33  41736  cdlemg38  41740  cdlemg44b  41757  cdlemk33N  41934  cdlemk34  41935  cdlemk38  41940  cdlemk35s-id  41963  cdlemk39s-id  41965  cdlemk53b  41981  cdlemk53  41982  cdlemk55  41986  cdlemk35u  41989  cdlemk55u  41991  cdleml3N  42003  cdlemn11pre  42235  aks6d1c1  43134