Theorem pm2.43a 55

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 23	. 2 ⊢ (𝜓 → 𝜓)
2		pm2.43a.1	. 2 ⊢ (𝜓 → (𝜑 → (𝜓 → 𝜒)))
3	1, 2	mpid 45	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  56  rspc  3578  rspc2gv  3600  intss1  4929  fvopab3ig  6983  suppimacnv  8166  odi  8560  nndi  8605  preleqALT  9582  inf3lem2  9594  zorn2lem7  10482  uzind2  12685  ssfzo12  13784  elfznelfzo  13798  injresinj  13816  suppssfz  14026  sqlecan  14241  fi1uzind  14540  cramerimplem2  22806  fiinopn  23023  uhgr0v0e  29525  0uhgrsubgr  29566  0uhgrrusgr  29865  ewlkprop  29890  usgrwwlks2on  30244  umgrwwlks2on  30245  3cyclfrgrrn1  30573  3cyclfrgrrn  30574  vdgn1frgrv2  30584  dvrunz  38488  ee223  45230  afveu  47774  afv2eu  47859  lindslinindsimp2  49123  nn0sumshdiglemB  49280