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  28993  ax5seg  29026  axpasch  29029  axeuclid  29051  br8d  32701  br8  35959  cgrextend  36211  segconeq  36213  trisegint  36231  ifscgr  36247  cgrsub  36248  cgrxfr  36258  lineext  36279  seglecgr12im  36313  segletr  36317  lineunray  36350  lineelsb2  36351  cvrcmp  39740  cvlatexch3  39795  cvlsupr2  39800  atcvrj2b  39889  atexchcvrN  39897  3dim1  39924  3dim2  39925  3atlem3  39942  3atlem5  39944  lplnnle2at  39998  2llnjaN  40023  4atlem3  40053  4atlem10b  40062  4atlem12  40069  2llnma3r  40245  paddasslem4  40280  paddasslem7  40283  paddasslem8  40284  paddasslem12  40288  paddasslem13  40289  paddasslem15  40291  pmodlem1  40303  pmodlem2  40304  atmod1i1m  40315  llnexchb2lem  40325  4atex2  40534  ltrnatlw  40640  trlval4  40645  arglem1N  40647  cdlemd4  40658  cdlemd5  40659  cdleme0moN  40682  cdleme16  40742  cdleme20  40781  cdleme21k  40795  cdleme27N  40826  cdleme28c  40829  cdleme43fsv1snlem  40877  cdleme38n  40921  cdleme40n  40925  cdleme41snaw  40933  cdlemg6c  41077  cdlemg8c  41086  cdlemg8  41088  cdlemg12e  41104  cdlemg16  41114  cdlemg16ALTN  41115  cdlemg16z  41116  cdlemg16zz  41117  cdlemg18a  41135  cdlemg20  41142  cdlemg22  41144  cdlemg37  41146  cdlemg31d  41157  cdlemg33  41168  cdlemg38  41172  cdlemg44b  41189  cdlemk38  41372  cdlemk35s-id  41395  cdlemk39s-id  41397  cdlemk53b  41413  cdlemk55  41418  cdlemk35u  41421  cdlemk55u  41423  cdlemn11pre  41667