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  8231  mulgdirlem  19020  nosupbnd2lem1  27655  noinfbnd2lem1  27670  brbtwn2  28885  ax5seglem3a  28910  ax5seg  28918  axpasch  28921  axeuclid  28943  br8d  32593  br8  35821  cgrextend  36073  segconeq  36075  segconeu  36076  trisegint  36093  ifscgr  36109  cgrsub  36110  cgrxfr  36120  lineext  36141  seglecgr12im  36175  segletr  36179  lineunray  36212  lineelsb2  36213  cvrcmp  39402  cvlsupr2  39462  atcvrj2b  39551  atexchcvrN  39559  3atlem3  39604  3atlem5  39606  lplnnle2at  39660  lplnllnneN  39675  4atlem3  39715  4atlem10b  39724  4atlem12  39731  2llnma3r  39907  paddasslem4  39942  paddasslem7  39945  paddasslem8  39946  paddasslem12  39950  paddasslem13  39951  paddasslem15  39953  pmodlem1  39965  pmodlem2  39966  atmod1i1m  39977  llnexchb2lem  39987  4atex2  40196  ltrnatlw  40302  arglem1N  40309  cdlemd4  40320  cdlemd5  40321  cdleme16  40404  cdleme20  40443  cdleme21k  40457  cdleme27N  40488  cdleme28c  40491  cdleme43fsv1snlem  40539  cdleme38n  40583  cdleme40n  40587  cdleme41snaw  40595  cdlemg6c  40739  cdlemg8c  40748  cdlemg8  40750  cdlemg12e  40766  cdlemg16ALTN  40777  cdlemg16zz  40779  cdlemg18a  40797  cdlemg20  40804  cdlemg22  40806  cdlemg37  40808  cdlemg31d  40819  cdlemg33  40830  cdlemg38  40834  cdlemg44b  40851  cdlemk33N  41028  cdlemk34  41029  cdlemk38  41034  cdlemk35s-id  41057  cdlemk39s-id  41059  cdlemk53b  41075  cdlemk53  41076  cdlemk55  41080  cdlemk35u  41083  cdlemk55u  41085  cdleml3N  41097  cdlemn11pre  41329  aks6d1c1  42229