Theorem simpl23 1251

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 1191	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜒)
2	1	3ad2antl2 1184	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  frrlem10  8095  mulgdirlem  18715  brbtwn2  27254  ax5seglem3a  27279  ax5seg  27287  axpasch  27290  axeuclid  27312  br8d  30929  br8  33702  nosupbnd2lem1  33897  noinfbnd2lem1  33912  cgrextend  34289  segconeq  34291  segconeu  34292  trisegint  34309  ifscgr  34325  cgrsub  34326  cgrxfr  34336  lineext  34357  seglecgr12im  34391  segletr  34395  lineunray  34428  lineelsb2  34429  cvrcmp  37276  cvlsupr2  37336  atcvrj2b  37425  atexchcvrN  37433  3atlem3  37478  3atlem5  37480  lplnnle2at  37534  lplnllnneN  37549  4atlem3  37589  4atlem10b  37598  4atlem12  37605  2llnma3r  37781  paddasslem4  37816  paddasslem7  37819  paddasslem8  37820  paddasslem12  37824  paddasslem13  37825  paddasslem15  37827  pmodlem1  37839  pmodlem2  37840  atmod1i1m  37851  llnexchb2lem  37861  4atex2  38070  ltrnatlw  38176  arglem1N  38183  cdlemd4  38194  cdlemd5  38195  cdleme16  38278  cdleme20  38317  cdleme21k  38331  cdleme27N  38362  cdleme28c  38365  cdleme43fsv1snlem  38413  cdleme38n  38457  cdleme40n  38461  cdleme41snaw  38469  cdlemg6c  38613  cdlemg8c  38622  cdlemg8  38624  cdlemg12e  38640  cdlemg16ALTN  38651  cdlemg16zz  38653  cdlemg18a  38671  cdlemg20  38678  cdlemg22  38680  cdlemg37  38682  cdlemg31d  38693  cdlemg33  38704  cdlemg38  38708  cdlemg44b  38725  cdlemk33N  38902  cdlemk34  38903  cdlemk38  38908  cdlemk35s-id  38931  cdlemk39s-id  38933  cdlemk53b  38949  cdlemk53  38950  cdlemk55  38954  cdlemk35u  38957  cdlemk55u  38959  cdleml3N  38971  cdlemn11pre  39203