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  29285  ax5seg  29318  axpasch  29321  axeuclid  29343  br8d  32983  br8  36261  cgrextend  36513  segconeq  36515  trisegint  36533  ifscgr  36549  cgrsub  36550  cgrxfr  36560  lineext  36581  seglecgr12im  36615  segletr  36619  lineunray  36652  lineelsb2  36653  cvrcmp  40090  cvlatexch3  40145  cvlsupr2  40150  atcvrj2b  40239  atexchcvrN  40247  3dim1  40274  3dim2  40275  3atlem3  40292  3atlem5  40294  lplnnle2at  40348  2llnjaN  40373  4atlem3  40403  4atlem10b  40412  4atlem12  40419  2llnma3r  40595  paddasslem4  40630  paddasslem7  40633  paddasslem8  40634  paddasslem12  40638  paddasslem13  40639  paddasslem15  40641  pmodlem1  40653  pmodlem2  40654  atmod1i1m  40665  llnexchb2lem  40675  4atex2  40884  ltrnatlw  40990  trlval4  40995  arglem1N  40997  cdlemd4  41008  cdlemd5  41009  cdleme0moN  41032  cdleme16  41092  cdleme20  41131  cdleme21k  41145  cdleme27N  41176  cdleme28c  41179  cdleme43fsv1snlem  41227  cdleme38n  41271  cdleme40n  41275  cdleme41snaw  41283  cdlemg6c  41427  cdlemg8c  41436  cdlemg8  41438  cdlemg12e  41454  cdlemg16  41464  cdlemg16ALTN  41465  cdlemg16z  41466  cdlemg16zz  41467  cdlemg18a  41485  cdlemg20  41492  cdlemg22  41494  cdlemg37  41496  cdlemg31d  41507  cdlemg33  41518  cdlemg38  41522  cdlemg44b  41539  cdlemk38  41722  cdlemk35s-id  41745  cdlemk39s-id  41747  cdlemk53b  41763  cdlemk55  41768  cdlemk35u  41771  cdlemk55u  41773  cdlemn11pre  42017