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  3515  rspc2gv  3536  intss1  4860  fvopab3ig  6792  suppimacnv  7894  odi  8285  nndi  8329  preleqALT  9210  inf3lem2  9222  pr2ne  9584  zorn2lem7  10081  uzind2  12235  ssfzo12  13300  elfznelfzo  13312  injresinj  13328  suppssfz  13532  sqlecan  13742  fi1uzind  14028  cramerimplem2  21535  fiinopn  21752  uhgr0v0e  27280  0uhgrsubgr  27321  0uhgrrusgr  27620  ewlkprop  27645  umgrwwlks2on  27995  3cyclfrgrrn1  28322  3cyclfrgrrn  28323  vdgn1frgrv2  28333  dvrunz  35798  ee223  41868  afveu  44260  afv2eu  44345  lindslinindsimp2  45420  nn0sumshdiglemB  45582