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  3567  rspc2gv  3589  intss1  4916  fvopab3ig  6930  suppimacnv  8114  odi  8504  nndi  8548  preleqALT  9532  inf3lem2  9544  zorn2lem7  10415  uzind2  12587  ssfzo12  13680  elfznelfzo  13693  injresinj  13709  suppssfz  13919  sqlecan  14134  fi1uzind  14432  cramerimplem2  22587  fiinopn  22804  uhgr0v0e  29201  0uhgrsubgr  29242  0uhgrrusgr  29542  ewlkprop  29567  umgrwwlks2on  29920  3cyclfrgrrn1  30247  3cyclfrgrrn  30248  vdgn1frgrv2  30258  dvrunz  37933  ee223  44608  afveu  47138  afv2eu  47223  lindslinindsimp2  48436  nn0sumshdiglemB  48593