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  3454  rspc2gv  3471  intss1  4626  fvopab3ig  6420  suppimacnv  7457  odi  7813  nndi  7857  preleqALT  8676  inf3lem2  8690  pr2ne  9028  zorn2lem7  9526  uzind2  11672  ssfzo12  12769  elfznelfzo  12781  injresinj  12797  suppssfz  13001  sqlecan  13178  fi1uzind  13481  cramerimplem2  20710  fiinopn  20926  uhgr0v0e  26353  0uhgrsubgr  26394  0uhgrrusgr  26709  ewlkprop  26734  umgrwwlks2on  27105  3cyclfrgrrn1  27467  3cyclfrgrrn  27468  vdgn1frgrv2  27478  dvrunz  34085  ee223  39384  afveu  41753  lindslinindsimp2  42780  nn0sumshdiglemB  42942