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  8344  mulgdirlem  19347  nosupbnd2lem1  28105  noinfbnd2lem1  28120  brbtwn2  29516  ax5seglem3a  29541  ax5seg  29549  axpasch  29552  axeuclid  29574  br8d  33277  br8  36712  cgrextend  36964  segconeq  36966  segconeu  36967  trisegint  36984  ifscgr  37000  cgrsub  37001  cgrxfr  37011  lineext  37032  seglecgr12im  37066  segletr  37070  lineunray  37103  lineelsb2  37104  cvrcmp  40543  cvlsupr2  40603  atcvrj2b  40692  atexchcvrN  40700  3atlem3  40745  3atlem5  40747  lplnnle2at  40801  lplnllnneN  40816  4atlem3  40856  4atlem10b  40865  4atlem12  40872  2llnma3r  41048  paddasslem4  41083  paddasslem7  41086  paddasslem8  41087  paddasslem12  41091  paddasslem13  41092  paddasslem15  41094  pmodlem1  41106  pmodlem2  41107  atmod1i1m  41118  llnexchb2lem  41128  4atex2  41337  ltrnatlw  41443  arglem1N  41450  cdlemd4  41461  cdlemd5  41462  cdleme16  41545  cdleme20  41584  cdleme21k  41598  cdleme27N  41629  cdleme28c  41632  cdleme43fsv1snlem  41680  cdleme38n  41724  cdleme40n  41728  cdleme41snaw  41736  cdlemg6c  41880  cdlemg8c  41889  cdlemg8  41891  cdlemg12e  41907  cdlemg16ALTN  41918  cdlemg16zz  41920  cdlemg18a  41938  cdlemg20  41945  cdlemg22  41947  cdlemg37  41949  cdlemg31d  41960  cdlemg33  41971  cdlemg38  41975  cdlemg44b  41992  cdlemk33N  42169  cdlemk34  42170  cdlemk38  42175  cdlemk35s-id  42198  cdlemk39s-id  42200  cdlemk53b  42216  cdlemk53  42217  cdlemk55  42221  cdlemk35u  42224  cdlemk55u  42226  cdleml3N  42238  cdlemn11pre  42470  aks6d1c1  43369