Theorem simpl22 1254

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  brbtwn2  28961  ax5seg  28994  axpasch  28997  axeuclid  29019  br8d  32668  br8  35931  cgrextend  36183  segconeq  36185  trisegint  36203  ifscgr  36219  cgrsub  36220  cgrxfr  36230  lineext  36251  seglecgr12im  36285  segletr  36289  lineunray  36322  lineelsb2  36323  cvrcmp  39580  cvlatexch3  39635  cvlsupr2  39640  atcvrj2b  39729  atexchcvrN  39737  3dim1  39764  3dim2  39765  3atlem3  39782  3atlem5  39784  lplnnle2at  39838  2llnjaN  39863  4atlem3  39893  4atlem10b  39902  4atlem12  39909  2llnma3r  40085  paddasslem4  40120  paddasslem7  40123  paddasslem8  40124  paddasslem12  40128  paddasslem13  40129  paddasslem15  40131  pmodlem1  40143  pmodlem2  40144  atmod1i1m  40155  llnexchb2lem  40165  4atex2  40374  ltrnatlw  40480  trlval4  40485  arglem1N  40487  cdlemd4  40498  cdlemd5  40499  cdleme0moN  40522  cdleme16  40582  cdleme20  40621  cdleme21k  40635  cdleme27N  40666  cdleme28c  40669  cdleme43fsv1snlem  40717  cdleme38n  40761  cdleme40n  40765  cdleme41snaw  40773  cdlemg6c  40917  cdlemg8c  40926  cdlemg8  40928  cdlemg12e  40944  cdlemg16  40954  cdlemg16ALTN  40955  cdlemg16z  40956  cdlemg16zz  40957  cdlemg18a  40975  cdlemg20  40982  cdlemg22  40984  cdlemg37  40986  cdlemg31d  40997  cdlemg33  41008  cdlemg38  41012  cdlemg44b  41029  cdlemk38  41212  cdlemk35s-id  41235  cdlemk39s-id  41237  cdlemk53b  41253  cdlemk55  41258  cdlemk35u  41261  cdlemk55u  41263  cdlemn11pre  41507