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  8235  mulgdirlem  19002  nosupbnd2lem1  27643  noinfbnd2lem1  27658  brbtwn2  28868  ax5seglem3a  28893  ax5seg  28901  axpasch  28904  axeuclid  28926  br8d  32571  br8  35728  cgrextend  35981  segconeq  35983  segconeu  35984  trisegint  36001  ifscgr  36017  cgrsub  36018  cgrxfr  36028  lineext  36049  seglecgr12im  36083  segletr  36087  lineunray  36120  lineelsb2  36121  cvrcmp  39261  cvlsupr2  39321  atcvrj2b  39411  atexchcvrN  39419  3atlem3  39464  3atlem5  39466  lplnnle2at  39520  lplnllnneN  39535  4atlem3  39575  4atlem10b  39584  4atlem12  39591  2llnma3r  39767  paddasslem4  39802  paddasslem7  39805  paddasslem8  39806  paddasslem12  39810  paddasslem13  39811  paddasslem15  39813  pmodlem1  39825  pmodlem2  39826  atmod1i1m  39837  llnexchb2lem  39847  4atex2  40056  ltrnatlw  40162  arglem1N  40169  cdlemd4  40180  cdlemd5  40181  cdleme16  40264  cdleme20  40303  cdleme21k  40317  cdleme27N  40348  cdleme28c  40351  cdleme43fsv1snlem  40399  cdleme38n  40443  cdleme40n  40447  cdleme41snaw  40455  cdlemg6c  40599  cdlemg8c  40608  cdlemg8  40610  cdlemg12e  40626  cdlemg16ALTN  40637  cdlemg16zz  40639  cdlemg18a  40657  cdlemg20  40664  cdlemg22  40666  cdlemg37  40668  cdlemg31d  40679  cdlemg33  40690  cdlemg38  40694  cdlemg44b  40711  cdlemk33N  40888  cdlemk34  40889  cdlemk38  40894  cdlemk35s-id  40917  cdlemk39s-id  40919  cdlemk53b  40935  cdlemk53  40936  cdlemk55  40940  cdlemk35u  40943  cdlemk55u  40945  cdleml3N  40957  cdlemn11pre  41189  aks6d1c1  42089