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  28962  ax5seg  28995  axpasch  28998  axeuclid  29020  br8d  32670  br8  35944  cgrextend  36196  segconeq  36198  trisegint  36216  ifscgr  36232  cgrsub  36233  cgrxfr  36243  lineext  36264  seglecgr12im  36298  segletr  36302  lineunray  36335  lineelsb2  36336  cvrcmp  39720  cvlatexch3  39775  cvlsupr2  39780  atcvrj2b  39869  atexchcvrN  39877  3dim1  39904  3dim2  39905  3atlem3  39922  3atlem5  39924  lplnnle2at  39978  2llnjaN  40003  4atlem3  40033  4atlem10b  40042  4atlem12  40049  2llnma3r  40225  paddasslem4  40260  paddasslem7  40263  paddasslem8  40264  paddasslem12  40268  paddasslem13  40269  paddasslem15  40271  pmodlem1  40283  pmodlem2  40284  atmod1i1m  40295  llnexchb2lem  40305  4atex2  40514  ltrnatlw  40620  trlval4  40625  arglem1N  40627  cdlemd4  40638  cdlemd5  40639  cdleme0moN  40662  cdleme16  40722  cdleme20  40761  cdleme21k  40775  cdleme27N  40806  cdleme28c  40809  cdleme43fsv1snlem  40857  cdleme38n  40901  cdleme40n  40905  cdleme41snaw  40913  cdlemg6c  41057  cdlemg8c  41066  cdlemg8  41068  cdlemg12e  41084  cdlemg16  41094  cdlemg16ALTN  41095  cdlemg16z  41096  cdlemg16zz  41097  cdlemg18a  41115  cdlemg20  41122  cdlemg22  41124  cdlemg37  41126  cdlemg31d  41137  cdlemg33  41148  cdlemg38  41152  cdlemg44b  41169  cdlemk38  41352  cdlemk35s-id  41375  cdlemk39s-id  41377  cdlemk53b  41393  cdlemk55  41398  cdlemk35u  41401  cdlemk55u  41403  cdlemn11pre  41647