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  3563  rspc2gv  3585  intss1  4911  fvopab3ig  6920  suppimacnv  8099  odi  8489  nndi  8533  preleqALT  9502  inf3lem2  9514  zorn2lem7  10385  uzind2  12558  ssfzo12  13651  elfznelfzo  13665  injresinj  13683  suppssfz  13893  sqlecan  14108  fi1uzind  14406  cramerimplem2  22592  fiinopn  22809  uhgr0v0e  29209  0uhgrsubgr  29250  0uhgrrusgr  29550  ewlkprop  29575  umgrwwlks2on  29928  3cyclfrgrrn1  30255  3cyclfrgrrn  30256  vdgn1frgrv2  30266  dvrunz  37973  ee223  44646  afveu  47163  afv2eu  47248  lindslinindsimp2  48474  nn0sumshdiglemB  48631