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  8316  mulgdirlem  19320  nosupbnd2lem1  28077  noinfbnd2lem1  28092  brbtwn2  29488  ax5seglem3a  29513  ax5seg  29521  axpasch  29524  axeuclid  29546  br8d  33249  br8  36613  cgrextend  36865  segconeq  36867  segconeu  36868  trisegint  36885  ifscgr  36901  cgrsub  36902  cgrxfr  36912  lineext  36933  seglecgr12im  36967  segletr  36971  lineunray  37004  lineelsb2  37005  cvrcmp  40433  cvlsupr2  40493  atcvrj2b  40582  atexchcvrN  40590  3atlem3  40635  3atlem5  40637  lplnnle2at  40691  lplnllnneN  40706  4atlem3  40746  4atlem10b  40755  4atlem12  40762  2llnma3r  40938  paddasslem4  40973  paddasslem7  40976  paddasslem8  40977  paddasslem12  40981  paddasslem13  40982  paddasslem15  40984  pmodlem1  40996  pmodlem2  40997  atmod1i1m  41008  llnexchb2lem  41018  4atex2  41227  ltrnatlw  41333  arglem1N  41340  cdlemd4  41351  cdlemd5  41352  cdleme16  41435  cdleme20  41474  cdleme21k  41488  cdleme27N  41519  cdleme28c  41522  cdleme43fsv1snlem  41570  cdleme38n  41614  cdleme40n  41618  cdleme41snaw  41626  cdlemg6c  41770  cdlemg8c  41779  cdlemg8  41781  cdlemg12e  41797  cdlemg16ALTN  41808  cdlemg16zz  41810  cdlemg18a  41828  cdlemg20  41835  cdlemg22  41837  cdlemg37  41839  cdlemg31d  41850  cdlemg33  41861  cdlemg38  41865  cdlemg44b  41882  cdlemk33N  42059  cdlemk34  42060  cdlemk38  42065  cdlemk35s-id  42088  cdlemk39s-id  42090  cdlemk53b  42106  cdlemk53  42107  cdlemk55  42111  cdlemk35u  42114  cdlemk55u  42116  cdleml3N  42128  cdlemn11pre  42360  aks6d1c1  43259