Theorem simpl22 1269

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  brbtwn2  29221  ax5seg  29254  axpasch  29257  axeuclid  29279  br8d  32919  br8  36214  cgrextend  36466  segconeq  36468  trisegint  36486  ifscgr  36502  cgrsub  36503  cgrxfr  36513  lineext  36534  seglecgr12im  36568  segletr  36572  lineunray  36605  lineelsb2  36606  cvrcmp  40025  cvlatexch3  40080  cvlsupr2  40085  atcvrj2b  40174  atexchcvrN  40182  3dim1  40209  3dim2  40210  3atlem3  40227  3atlem5  40229  lplnnle2at  40283  2llnjaN  40308  4atlem3  40338  4atlem10b  40347  4atlem12  40354  2llnma3r  40530  paddasslem4  40565  paddasslem7  40568  paddasslem8  40569  paddasslem12  40573  paddasslem13  40574  paddasslem15  40576  pmodlem1  40588  pmodlem2  40589  atmod1i1m  40600  llnexchb2lem  40610  4atex2  40819  ltrnatlw  40925  trlval4  40930  arglem1N  40932  cdlemd4  40943  cdlemd5  40944  cdleme0moN  40967  cdleme16  41027  cdleme20  41066  cdleme21k  41080  cdleme27N  41111  cdleme28c  41114  cdleme43fsv1snlem  41162  cdleme38n  41206  cdleme40n  41210  cdleme41snaw  41218  cdlemg6c  41362  cdlemg8c  41371  cdlemg8  41373  cdlemg12e  41389  cdlemg16  41399  cdlemg16ALTN  41400  cdlemg16z  41401  cdlemg16zz  41402  cdlemg18a  41420  cdlemg20  41427  cdlemg22  41429  cdlemg37  41431  cdlemg31d  41442  cdlemg33  41453  cdlemg38  41457  cdlemg44b  41474  cdlemk38  41657  cdlemk35s-id  41680  cdlemk39s-id  41682  cdlemk53b  41698  cdlemk55  41703  cdlemk35u  41706  cdlemk55u  41708  cdlemn11pre  41952