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  3565  rspc2gv  3587  intss1  4919  fvopab3ig  6938  suppimacnv  8118  odi  8508  nndi  8553  preleqALT  9530  inf3lem2  9542  zorn2lem7  10416  uzind2  12589  ssfzo12  13679  elfznelfzo  13693  injresinj  13711  suppssfz  13921  sqlecan  14136  fi1uzind  14434  cramerimplem2  22632  fiinopn  22849  uhgr0v0e  29294  0uhgrsubgr  29335  0uhgrrusgr  29635  ewlkprop  29660  usgrwwlks2on  30014  umgrwwlks2on  30015  3cyclfrgrrn1  30343  3cyclfrgrrn  30344  vdgn1frgrv2  30354  dvrunz  38126  ee223  44911  afveu  47435  afv2eu  47520  lindslinindsimp2  48745  nn0sumshdiglemB  48902