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  3553  rspc2gv  3575  intss1  4906  fvopab3ig  6935  suppimacnv  8115  odi  8505  nndi  8550  preleqALT  9527  inf3lem2  9539  zorn2lem7  10413  uzind2  12611  ssfzo12  13703  elfznelfzo  13717  injresinj  13735  suppssfz  13945  sqlecan  14160  fi1uzind  14458  cramerimplem2  22658  fiinopn  22875  uhgr0v0e  29326  0uhgrsubgr  29367  0uhgrrusgr  29667  ewlkprop  29692  usgrwwlks2on  30046  umgrwwlks2on  30047  3cyclfrgrrn1  30375  3cyclfrgrrn  30376  vdgn1frgrv2  30386  dvrunz  38286  ee223  45076  afveu  47598  afv2eu  47683  lindslinindsimp2  48936  nn0sumshdiglemB  49093