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  3610  rspc2gv  3632  intss1  4968  fvopab3ig  7012  suppimacnv  8198  odi  8616  nndi  8660  preleqALT  9655  inf3lem2  9667  pr2neOLD  10043  zorn2lem7  10540  uzind2  12709  ssfzo12  13795  elfznelfzo  13808  injresinj  13824  suppssfz  14032  sqlecan  14245  fi1uzind  14543  cramerimplem2  22706  fiinopn  22923  uhgr0v0e  29270  0uhgrsubgr  29311  0uhgrrusgr  29611  ewlkprop  29636  umgrwwlks2on  29987  3cyclfrgrrn1  30314  3cyclfrgrrn  30315  vdgn1frgrv2  30325  dvrunz  37941  ee223  44632  afveu  47103  afv2eu  47188  lindslinindsimp2  48309  nn0sumshdiglemB  48470