Theorem simpl22 1271

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  brbtwn2  29370  ax5seg  29403  axpasch  29406  axeuclid  29428  br8d  33089  br8  36343  cgrextend  36596  segconeq  36598  trisegint  36616  ifscgr  36632  cgrsub  36633  cgrxfr  36643  lineext  36664  seglecgr12im  36698  segletr  36702  lineunray  36735  lineelsb2  36736  cvrcmp  40164  cvlatexch3  40219  cvlsupr2  40224  atcvrj2b  40313  atexchcvrN  40321  3dim1  40348  3dim2  40349  3atlem3  40366  3atlem5  40368  lplnnle2at  40422  2llnjaN  40447  4atlem3  40477  4atlem10b  40486  4atlem12  40493  2llnma3r  40669  paddasslem4  40704  paddasslem7  40707  paddasslem8  40708  paddasslem12  40712  paddasslem13  40713  paddasslem15  40715  pmodlem1  40727  pmodlem2  40728  atmod1i1m  40739  llnexchb2lem  40749  4atex2  40958  ltrnatlw  41064  trlval4  41069  arglem1N  41071  cdlemd4  41082  cdlemd5  41083  cdleme0moN  41106  cdleme16  41166  cdleme20  41205  cdleme21k  41219  cdleme27N  41250  cdleme28c  41253  cdleme43fsv1snlem  41301  cdleme38n  41345  cdleme40n  41349  cdleme41snaw  41357  cdlemg6c  41501  cdlemg8c  41510  cdlemg8  41512  cdlemg12e  41528  cdlemg16  41538  cdlemg16ALTN  41539  cdlemg16z  41540  cdlemg16zz  41541  cdlemg18a  41559  cdlemg20  41566  cdlemg22  41568  cdlemg37  41570  cdlemg31d  41581  cdlemg33  41592  cdlemg38  41596  cdlemg44b  41613  cdlemk38  41796  cdlemk35s-id  41819  cdlemk39s-id  41821  cdlemk53b  41837  cdlemk55  41842  cdlemk35u  41845  cdlemk55u  41847  cdlemn11pre  42091