Theorem simpl22 1254

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  brbtwn2  28990  ax5seg  29023  axpasch  29026  axeuclid  29048  br8d  32697  br8  35969  cgrextend  36221  segconeq  36223  trisegint  36241  ifscgr  36257  cgrsub  36258  cgrxfr  36268  lineext  36289  seglecgr12im  36323  segletr  36327  lineunray  36360  lineelsb2  36361  cvrcmp  39648  cvlatexch3  39703  cvlsupr2  39708  atcvrj2b  39797  atexchcvrN  39805  3dim1  39832  3dim2  39833  3atlem3  39850  3atlem5  39852  lplnnle2at  39906  2llnjaN  39931  4atlem3  39961  4atlem10b  39970  4atlem12  39977  2llnma3r  40153  paddasslem4  40188  paddasslem7  40191  paddasslem8  40192  paddasslem12  40196  paddasslem13  40197  paddasslem15  40199  pmodlem1  40211  pmodlem2  40212  atmod1i1m  40223  llnexchb2lem  40233  4atex2  40442  ltrnatlw  40548  trlval4  40553  arglem1N  40555  cdlemd4  40566  cdlemd5  40567  cdleme0moN  40590  cdleme16  40650  cdleme20  40689  cdleme21k  40703  cdleme27N  40734  cdleme28c  40737  cdleme43fsv1snlem  40785  cdleme38n  40829  cdleme40n  40833  cdleme41snaw  40841  cdlemg6c  40985  cdlemg8c  40994  cdlemg8  40996  cdlemg12e  41012  cdlemg16  41022  cdlemg16ALTN  41023  cdlemg16z  41024  cdlemg16zz  41025  cdlemg18a  41043  cdlemg20  41050  cdlemg22  41052  cdlemg37  41054  cdlemg31d  41065  cdlemg33  41076  cdlemg38  41080  cdlemg44b  41097  cdlemk38  41280  cdlemk35s-id  41303  cdlemk39s-id  41305  cdlemk53b  41321  cdlemk55  41326  cdlemk35u  41329  cdlemk55u  41331  cdlemn11pre  41575