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  3553  rspc2gv  3571  intss1  4797  fvopab3ig  6631  suppimacnv  7692  odi  8055  nndi  8099  preleqALT  8926  inf3lem2  8938  pr2ne  9277  zorn2lem7  9770  uzind2  11924  ssfzo12  12980  elfznelfzo  12992  injresinj  13008  suppssfz  13212  sqlecan  13421  fi1uzind  13701  cramerimplem2  20977  fiinopn  21193  uhgr0v0e  26703  0uhgrsubgr  26744  0uhgrrusgr  27043  ewlkprop  27068  umgrwwlks2on  27423  3cyclfrgrrn1  27756  3cyclfrgrrn  27757  vdgn1frgrv2  27767  dvrunz  34764  ee223  40507  afveu  42868  afv2eu  42953  lindslinindsimp2  43998  nn0sumshdiglemB  44161