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 394   ∧ 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 395  df-3an 1087

This theorem is referenced by:  frrlem10  8282  mulgdirlem  19021  nosupbnd2lem1  27454  noinfbnd2lem1  27469  brbtwn2  28430  ax5seglem3a  28455  ax5seg  28463  axpasch  28466  axeuclid  28488  br8d  32106  br8  35030  cgrextend  35284  segconeq  35286  segconeu  35287  trisegint  35304  ifscgr  35320  cgrsub  35321  cgrxfr  35331  lineext  35352  seglecgr12im  35386  segletr  35390  lineunray  35423  lineelsb2  35424  cvrcmp  38456  cvlsupr2  38516  atcvrj2b  38606  atexchcvrN  38614  3atlem3  38659  3atlem5  38661  lplnnle2at  38715  lplnllnneN  38730  4atlem3  38770  4atlem10b  38779  4atlem12  38786  2llnma3r  38962  paddasslem4  38997  paddasslem7  39000  paddasslem8  39001  paddasslem12  39005  paddasslem13  39006  paddasslem15  39008  pmodlem1  39020  pmodlem2  39021  atmod1i1m  39032  llnexchb2lem  39042  4atex2  39251  ltrnatlw  39357  arglem1N  39364  cdlemd4  39375  cdlemd5  39376  cdleme16  39459  cdleme20  39498  cdleme21k  39512  cdleme27N  39543  cdleme28c  39546  cdleme43fsv1snlem  39594  cdleme38n  39638  cdleme40n  39642  cdleme41snaw  39650  cdlemg6c  39794  cdlemg8c  39803  cdlemg8  39805  cdlemg12e  39821  cdlemg16ALTN  39832  cdlemg16zz  39834  cdlemg18a  39852  cdlemg20  39859  cdlemg22  39861  cdlemg37  39863  cdlemg31d  39874  cdlemg33  39885  cdlemg38  39889  cdlemg44b  39906  cdlemk33N  40083  cdlemk34  40084  cdlemk38  40089  cdlemk35s-id  40112  cdlemk39s-id  40114  cdlemk53b  40130  cdlemk53  40131  cdlemk55  40135  cdlemk35u  40138  cdlemk55u  40140  cdleml3N  40152  cdlemn11pre  40384