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  29513  ax5seg  29546  axpasch  29549  axeuclid  29571  br8d  33274  br8  36699  cgrextend  36951  segconeq  36953  trisegint  36971  ifscgr  36987  cgrsub  36988  cgrxfr  36998  lineext  37019  seglecgr12im  37053  segletr  37057  lineunray  37090  lineelsb2  37091  cvrcmp  40532  cvlatexch3  40587  cvlsupr2  40592  atcvrj2b  40681  atexchcvrN  40689  3dim1  40716  3dim2  40717  3atlem3  40734  3atlem5  40736  lplnnle2at  40790  2llnjaN  40815  4atlem3  40845  4atlem10b  40854  4atlem12  40861  2llnma3r  41037  paddasslem4  41072  paddasslem7  41075  paddasslem8  41076  paddasslem12  41080  paddasslem13  41081  paddasslem15  41083  pmodlem1  41095  pmodlem2  41096  atmod1i1m  41107  llnexchb2lem  41117  4atex2  41326  ltrnatlw  41432  trlval4  41437  arglem1N  41439  cdlemd4  41450  cdlemd5  41451  cdleme0moN  41474  cdleme16  41534  cdleme20  41573  cdleme21k  41587  cdleme27N  41618  cdleme28c  41621  cdleme43fsv1snlem  41669  cdleme38n  41713  cdleme40n  41717  cdleme41snaw  41725  cdlemg6c  41869  cdlemg8c  41878  cdlemg8  41880  cdlemg12e  41896  cdlemg16  41906  cdlemg16ALTN  41907  cdlemg16z  41908  cdlemg16zz  41909  cdlemg18a  41927  cdlemg20  41934  cdlemg22  41936  cdlemg37  41938  cdlemg31d  41949  cdlemg33  41960  cdlemg38  41964  cdlemg44b  41981  cdlemk38  42164  cdlemk35s-id  42187  cdlemk39s-id  42189  cdlemk53b  42205  cdlemk55  42210  cdlemk35u  42213  cdlemk55u  42215  cdlemn11pre  42459