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  3623  rspc2gv  3645  intss1  4987  fvopab3ig  7025  suppimacnv  8215  odi  8635  nndi  8679  preleqALT  9686  inf3lem2  9698  pr2neOLD  10074  zorn2lem7  10571  uzind2  12736  ssfzo12  13809  elfznelfzo  13822  injresinj  13838  suppssfz  14045  sqlecan  14258  fi1uzind  14556  cramerimplem2  22711  fiinopn  22928  uhgr0v0e  29273  0uhgrsubgr  29314  0uhgrrusgr  29614  ewlkprop  29639  umgrwwlks2on  29990  3cyclfrgrrn1  30317  3cyclfrgrrn  30318  vdgn1frgrv2  30328  dvrunz  37914  ee223  44605  afveu  47068  afv2eu  47153  lindslinindsimp2  48192  nn0sumshdiglemB  48354