Theorem simpl23 1254

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 1194	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜒)
2	1	3ad2antl2 1187	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  8294  mulgdirlem  19088  nosupbnd2lem1  27679  noinfbnd2lem1  27694  brbtwn2  28884  ax5seglem3a  28909  ax5seg  28917  axpasch  28920  axeuclid  28942  br8d  32590  br8  35773  cgrextend  36026  segconeq  36028  segconeu  36029  trisegint  36046  ifscgr  36062  cgrsub  36063  cgrxfr  36073  lineext  36094  seglecgr12im  36128  segletr  36132  lineunray  36165  lineelsb2  36166  cvrcmp  39301  cvlsupr2  39361  atcvrj2b  39451  atexchcvrN  39459  3atlem3  39504  3atlem5  39506  lplnnle2at  39560  lplnllnneN  39575  4atlem3  39615  4atlem10b  39624  4atlem12  39631  2llnma3r  39807  paddasslem4  39842  paddasslem7  39845  paddasslem8  39846  paddasslem12  39850  paddasslem13  39851  paddasslem15  39853  pmodlem1  39865  pmodlem2  39866  atmod1i1m  39877  llnexchb2lem  39887  4atex2  40096  ltrnatlw  40202  arglem1N  40209  cdlemd4  40220  cdlemd5  40221  cdleme16  40304  cdleme20  40343  cdleme21k  40357  cdleme27N  40388  cdleme28c  40391  cdleme43fsv1snlem  40439  cdleme38n  40483  cdleme40n  40487  cdleme41snaw  40495  cdlemg6c  40639  cdlemg8c  40648  cdlemg8  40650  cdlemg12e  40666  cdlemg16ALTN  40677  cdlemg16zz  40679  cdlemg18a  40697  cdlemg20  40704  cdlemg22  40706  cdlemg37  40708  cdlemg31d  40719  cdlemg33  40730  cdlemg38  40734  cdlemg44b  40751  cdlemk33N  40928  cdlemk34  40929  cdlemk38  40934  cdlemk35s-id  40957  cdlemk39s-id  40959  cdlemk53b  40975  cdlemk53  40976  cdlemk55  40980  cdlemk35u  40983  cdlemk55u  40985  cdleml3N  40997  cdlemn11pre  41229  aks6d1c1  42129