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  28974  ax5seg  29007  axpasch  29010  axeuclid  29032  br8d  32681  br8  35938  cgrextend  36190  segconeq  36192  trisegint  36210  ifscgr  36226  cgrsub  36227  cgrxfr  36237  lineext  36258  seglecgr12im  36292  segletr  36296  lineunray  36329  lineelsb2  36330  cvrcmp  39729  cvlatexch3  39784  cvlsupr2  39789  atcvrj2b  39878  atexchcvrN  39886  3dim1  39913  3dim2  39914  3atlem3  39931  3atlem5  39933  lplnnle2at  39987  2llnjaN  40012  4atlem3  40042  4atlem10b  40051  4atlem12  40058  2llnma3r  40234  paddasslem4  40269  paddasslem7  40272  paddasslem8  40273  paddasslem12  40277  paddasslem13  40278  paddasslem15  40280  pmodlem1  40292  pmodlem2  40293  atmod1i1m  40304  llnexchb2lem  40314  4atex2  40523  ltrnatlw  40629  trlval4  40634  arglem1N  40636  cdlemd4  40647  cdlemd5  40648  cdleme0moN  40671  cdleme16  40731  cdleme20  40770  cdleme21k  40784  cdleme27N  40815  cdleme28c  40818  cdleme43fsv1snlem  40866  cdleme38n  40910  cdleme40n  40914  cdleme41snaw  40922  cdlemg6c  41066  cdlemg8c  41075  cdlemg8  41077  cdlemg12e  41093  cdlemg16  41103  cdlemg16ALTN  41104  cdlemg16z  41105  cdlemg16zz  41106  cdlemg18a  41124  cdlemg20  41131  cdlemg22  41133  cdlemg37  41135  cdlemg31d  41146  cdlemg33  41157  cdlemg38  41161  cdlemg44b  41178  cdlemk38  41361  cdlemk35s-id  41384  cdlemk39s-id  41386  cdlemk53b  41402  cdlemk55  41407  cdlemk35u  41410  cdlemk55u  41412  cdlemn11pre  41656