Theorem simpl31 1140

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

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

Proof of Theorem simpl31

Step	Hyp	Ref	Expression
1		simp31 1095	. 2 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜑)
2	1	adantr 481	1 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1036

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 197  df-an 386  df-3an 1038

This theorem is referenced by:  ax5seglem3a  25710  ax5seg  25718  uhgrwkspth  26520  usgr2wlkspth  26524  br8d  29262  br8  31351  nosires  31574  cgrextend  31754  segconeq  31756  trisegint  31774  ifscgr  31790  cgrsub  31791  btwnxfr  31802  seglecgr12im  31856  segletr  31860  atbtwn  34209  3dim1  34230  2llnjaN  34329  4atlem10b  34368  4atlem11  34372  4atlem12  34375  2lplnj  34383  paddasslem4  34586  pmodlem1  34609  4atex2  34840  trlval3  34951  arglem1N  34954  cdleme0moN  34989  cdleme17b  35051  cdleme20  35089  cdleme21j  35101  cdleme28c  35137  cdleme35h2  35222  cdlemg6c  35385  cdlemg6  35388  cdlemg7N  35391  cdlemg8c  35394  cdlemg11a  35402  cdlemg11b  35407  cdlemg12e  35412  cdlemg16  35422  cdlemg16ALTN  35423  cdlemg16zz  35425  cdlemg20  35450  cdlemg22  35452  cdlemg37  35454  cdlemg31d  35465  cdlemg33b  35472  cdlemg33  35476  cdlemg39  35481  cdlemg42  35494  cdlemk25-3  35669  cdlemk33N  35674  cdlemk53b  35721