Theorem simpl31 1255

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

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

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 1088

This theorem is referenced by:  nosupres  27619  noinfres  27634  ax5seglem3a  28857  ax5seg  28865  uhgrwkspth  29685  usgr2wlkspth  29689  br8d  32538  br8  35743  cgrextend  35996  segconeq  35998  trisegint  36016  ifscgr  36032  cgrsub  36033  btwnxfr  36044  seglecgr12im  36098  segletr  36102  atbtwn  39440  3dim1  39461  2llnjaN  39560  4atlem10b  39599  4atlem11  39603  4atlem12  39606  2lplnj  39614  paddasslem4  39817  pmodlem1  39840  4atex2  40071  trlval3  40181  arglem1N  40184  cdleme0moN  40219  cdleme17b  40281  cdleme20  40318  cdleme21j  40330  cdleme28c  40366  cdleme35h2  40451  cdlemg6c  40614  cdlemg6  40617  cdlemg7N  40620  cdlemg8c  40623  cdlemg11a  40631  cdlemg11b  40636  cdlemg12e  40641  cdlemg16  40651  cdlemg16ALTN  40652  cdlemg16zz  40654  cdlemg20  40679  cdlemg22  40681  cdlemg37  40683  cdlemg31d  40694  cdlemg33b  40701  cdlemg33  40705  cdlemg39  40710  cdlemg42  40723  cdlemk25-3  40898  cdlemk33N  40903  cdlemk53b  40950