Theorem simpl23 1253

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 1193	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜒)
2	1	3ad2antl2 1186	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  8302  mulgdirlem  19093  nosupbnd2lem1  27697  noinfbnd2lem1  27712  brbtwn2  28851  ax5seglem3a  28876  ax5seg  28884  axpasch  28887  axeuclid  28909  br8d  32558  br8  35731  cgrextend  35984  segconeq  35986  segconeu  35987  trisegint  36004  ifscgr  36020  cgrsub  36021  cgrxfr  36031  lineext  36052  seglecgr12im  36086  segletr  36090  lineunray  36123  lineelsb2  36124  cvrcmp  39259  cvlsupr2  39319  atcvrj2b  39409  atexchcvrN  39417  3atlem3  39462  3atlem5  39464  lplnnle2at  39518  lplnllnneN  39533  4atlem3  39573  4atlem10b  39582  4atlem12  39589  2llnma3r  39765  paddasslem4  39800  paddasslem7  39803  paddasslem8  39804  paddasslem12  39808  paddasslem13  39809  paddasslem15  39811  pmodlem1  39823  pmodlem2  39824  atmod1i1m  39835  llnexchb2lem  39845  4atex2  40054  ltrnatlw  40160  arglem1N  40167  cdlemd4  40178  cdlemd5  40179  cdleme16  40262  cdleme20  40301  cdleme21k  40315  cdleme27N  40346  cdleme28c  40349  cdleme43fsv1snlem  40397  cdleme38n  40441  cdleme40n  40445  cdleme41snaw  40453  cdlemg6c  40597  cdlemg8c  40606  cdlemg8  40608  cdlemg12e  40624  cdlemg16ALTN  40635  cdlemg16zz  40637  cdlemg18a  40655  cdlemg20  40662  cdlemg22  40664  cdlemg37  40666  cdlemg31d  40677  cdlemg33  40688  cdlemg38  40692  cdlemg44b  40709  cdlemk33N  40886  cdlemk34  40887  cdlemk38  40892  cdlemk35s-id  40915  cdlemk39s-id  40917  cdlemk53b  40933  cdlemk53  40934  cdlemk55  40938  cdlemk35u  40941  cdlemk55u  40943  cdleml3N  40955  cdlemn11pre  41187  aks6d1c1  42092