Theorem simpl22 1252

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)

Assertion

Ref	Expression
simpl22	⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Proof of Theorem simpl22

Step	Hyp	Ref	Expression
1		simpl2 1192	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜓)
2	1	3ad2antl2 1186	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜓)

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

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

This theorem is referenced by:  brbtwn2  28418  ax5seg  28451  axpasch  28454  axeuclid  28476  br8d  32094  br8  35018  cgrextend  35272  segconeq  35274  trisegint  35292  ifscgr  35308  cgrsub  35309  cgrxfr  35319  lineext  35340  seglecgr12im  35374  segletr  35378  lineunray  35411  lineelsb2  35412  cvrcmp  38456  cvlatexch3  38511  cvlsupr2  38516  atcvrj2b  38606  atexchcvrN  38614  3dim1  38641  3dim2  38642  3atlem3  38659  3atlem5  38661  lplnnle2at  38715  2llnjaN  38740  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  trlval4  39362  arglem1N  39364  cdlemd4  39375  cdlemd5  39376  cdleme0moN  39399  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  cdlemg16  39831  cdlemg16ALTN  39832  cdlemg16z  39833  cdlemg16zz  39834  cdlemg18a  39852  cdlemg20  39859  cdlemg22  39861  cdlemg37  39863  cdlemg31d  39874  cdlemg33  39885  cdlemg38  39889  cdlemg44b  39906  cdlemk38  40089  cdlemk35s-id  40112  cdlemk39s-id  40114  cdlemk53b  40130  cdlemk55  40135  cdlemk35u  40138  cdlemk55u  40140  cdlemn11pre  40384