Theorem pm2.43a 54

Description: Inference absorbing redundant antecedent. (Contributed by NM, 7-Nov-1995.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.)

Hypothesis

Ref	Expression
pm2.43a.1	⊢ (𝜓 → (𝜑 → (𝜓 → 𝜒)))

Assertion

Ref	Expression
pm2.43a	⊢ (𝜓 → (𝜑 → 𝜒))

Proof of Theorem pm2.43a

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜓 → 𝜓)
2		pm2.43a.1	. 2 ⊢ (𝜓 → (𝜑 → (𝜓 → 𝜒)))
3	1, 2	mpid 44	1 ⊢ (𝜓 → (𝜑 → 𝜒))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  pm2.43b  55  rspc  3555  rspc2gv  3577  intss1  4900  fvopab3ig  6938  suppimacnv  8121  odi  8511  nndi  8556  preleqALT  9536  inf3lem2  9548  zorn2lem7  10422  uzind2  12620  ssfzo12  13712  elfznelfzo  13726  injresinj  13744  suppssfz  13954  sqlecan  14169  fi1uzind  14467  cramerimplem2  22674  fiinopn  22891  uhgr0v0e  29332  0uhgrsubgr  29373  0uhgrrusgr  29672  ewlkprop  29697  usgrwwlks2on  30051  umgrwwlks2on  30052  3cyclfrgrrn1  30380  3cyclfrgrrn  30381  vdgn1frgrv2  30391  dvrunz  38322  ee223  45079  afveu  47617  afv2eu  47702  lindslinindsimp2  48955  nn0sumshdiglemB  49112