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  29488  ax5seg  29521  axpasch  29524  axeuclid  29546  br8d  33249  br8  36613  cgrextend  36865  segconeq  36867  trisegint  36885  ifscgr  36901  cgrsub  36902  cgrxfr  36912  lineext  36933  seglecgr12im  36967  segletr  36971  lineunray  37004  lineelsb2  37005  cvrcmp  40433  cvlatexch3  40488  cvlsupr2  40493  atcvrj2b  40582  atexchcvrN  40590  3dim1  40617  3dim2  40618  3atlem3  40635  3atlem5  40637  lplnnle2at  40691  2llnjaN  40716  4atlem3  40746  4atlem10b  40755  4atlem12  40762  2llnma3r  40938  paddasslem4  40973  paddasslem7  40976  paddasslem8  40977  paddasslem12  40981  paddasslem13  40982  paddasslem15  40984  pmodlem1  40996  pmodlem2  40997  atmod1i1m  41008  llnexchb2lem  41018  4atex2  41227  ltrnatlw  41333  trlval4  41338  arglem1N  41340  cdlemd4  41351  cdlemd5  41352  cdleme0moN  41375  cdleme16  41435  cdleme20  41474  cdleme21k  41488  cdleme27N  41519  cdleme28c  41522  cdleme43fsv1snlem  41570  cdleme38n  41614  cdleme40n  41618  cdleme41snaw  41626  cdlemg6c  41770  cdlemg8c  41779  cdlemg8  41781  cdlemg12e  41797  cdlemg16  41807  cdlemg16ALTN  41808  cdlemg16z  41809  cdlemg16zz  41810  cdlemg18a  41828  cdlemg20  41835  cdlemg22  41837  cdlemg37  41839  cdlemg31d  41850  cdlemg33  41861  cdlemg38  41865  cdlemg44b  41882  cdlemk38  42065  cdlemk35s-id  42088  cdlemk39s-id  42090  cdlemk53b  42106  cdlemk55  42111  cdlemk35u  42114  cdlemk55u  42116  cdlemn11pre  42360