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  3589  rspc2gv  3611  intss1  4939  fvopab3ig  6982  suppimacnv  8173  odi  8591  nndi  8635  preleqALT  9631  inf3lem2  9643  pr2neOLD  10019  zorn2lem7  10516  uzind2  12686  ssfzo12  13775  elfznelfzo  13788  injresinj  13804  suppssfz  14012  sqlecan  14227  fi1uzind  14525  cramerimplem2  22622  fiinopn  22839  uhgr0v0e  29217  0uhgrsubgr  29258  0uhgrrusgr  29558  ewlkprop  29583  umgrwwlks2on  29939  3cyclfrgrrn1  30266  3cyclfrgrrn  30267  vdgn1frgrv2  30277  dvrunz  37978  ee223  44659  afveu  47182  afv2eu  47267  lindslinindsimp2  48439  nn0sumshdiglemB  48600