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  3595  rspc2gv  3617  intss1  4966  fvopab3ig  6998  suppimacnv  8177  odi  8598  nndi  8642  preleqALT  9640  inf3lem2  9652  pr2neOLD  10028  zorn2lem7  10525  uzind2  12685  ssfzo12  13757  elfznelfzo  13769  injresinj  13785  suppssfz  13991  sqlecan  14204  fi1uzind  14490  cramerimplem2  22616  fiinopn  22833  uhgr0v0e  29107  0uhgrsubgr  29148  0uhgrrusgr  29448  ewlkprop  29473  umgrwwlks2on  29824  3cyclfrgrrn1  30151  3cyclfrgrrn  30152  vdgn1frgrv2  30162  dvrunz  37497  ee223  44138  afveu  46596  afv2eu  46681  lindslinindsimp2  47643  nn0sumshdiglemB  47805