Theorem simpl23 1260

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  frrlem10  8242  mulgdirlem  19079  nosupbnd2lem1  27704  noinfbnd2lem1  27719  brbtwn2  28999  ax5seglem3a  29024  ax5seg  29032  axpasch  29035  axeuclid  29057  br8d  32707  br8  35991  cgrextend  36243  segconeq  36245  segconeu  36246  trisegint  36263  ifscgr  36279  cgrsub  36280  cgrxfr  36290  lineext  36311  seglecgr12im  36345  segletr  36349  lineunray  36382  lineelsb2  36383  cvrcmp  39782  cvlsupr2  39842  atcvrj2b  39931  atexchcvrN  39939  3atlem3  39984  3atlem5  39986  lplnnle2at  40040  lplnllnneN  40055  4atlem3  40095  4atlem10b  40104  4atlem12  40111  2llnma3r  40287  paddasslem4  40322  paddasslem7  40325  paddasslem8  40326  paddasslem12  40330  paddasslem13  40331  paddasslem15  40333  pmodlem1  40345  pmodlem2  40346  atmod1i1m  40357  llnexchb2lem  40367  4atex2  40576  ltrnatlw  40682  arglem1N  40689  cdlemd4  40700  cdlemd5  40701  cdleme16  40784  cdleme20  40823  cdleme21k  40837  cdleme27N  40868  cdleme28c  40871  cdleme43fsv1snlem  40919  cdleme38n  40963  cdleme40n  40967  cdleme41snaw  40975  cdlemg6c  41119  cdlemg8c  41128  cdlemg8  41130  cdlemg12e  41146  cdlemg16ALTN  41157  cdlemg16zz  41159  cdlemg18a  41177  cdlemg20  41184  cdlemg22  41186  cdlemg37  41188  cdlemg31d  41199  cdlemg33  41210  cdlemg38  41214  cdlemg44b  41231  cdlemk33N  41408  cdlemk34  41409  cdlemk38  41414  cdlemk35s-id  41437  cdlemk39s-id  41439  cdlemk53b  41455  cdlemk53  41456  cdlemk55  41460  cdlemk35u  41463  cdlemk55u  41465  cdleml3N  41477  cdlemn11pre  41709  aks6d1c1  42608