Theorem simpl31 1254

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)

Assertion

Ref	Expression
simpl31	⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜑)

Proof of Theorem simpl31

Step	Hyp	Ref	Expression
1		simpl1 1191	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜑)
2	1	3ad2antl3 1187	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:  nosupres  27770  noinfres  27785  ax5seglem3a  28963  ax5seg  28971  uhgrwkspth  29791  usgr2wlkspth  29795  br8d  32632  br8  35718  cgrextend  35972  segconeq  35974  trisegint  35992  ifscgr  36008  cgrsub  36009  btwnxfr  36020  seglecgr12im  36074  segletr  36078  atbtwn  39403  3dim1  39424  2llnjaN  39523  4atlem10b  39562  4atlem11  39566  4atlem12  39569  2lplnj  39577  paddasslem4  39780  pmodlem1  39803  4atex2  40034  trlval3  40144  arglem1N  40147  cdleme0moN  40182  cdleme17b  40244  cdleme20  40281  cdleme21j  40293  cdleme28c  40329  cdleme35h2  40414  cdlemg6c  40577  cdlemg6  40580  cdlemg7N  40583  cdlemg8c  40586  cdlemg11a  40594  cdlemg11b  40599  cdlemg12e  40604  cdlemg16  40614  cdlemg16ALTN  40615  cdlemg16zz  40617  cdlemg20  40642  cdlemg22  40644  cdlemg37  40646  cdlemg31d  40657  cdlemg33b  40664  cdlemg33  40668  cdlemg39  40673  cdlemg42  40686  cdlemk25-3  40861  cdlemk33N  40866  cdlemk53b  40913