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  3576  rspc2gv  3598  intss1  4927  fvopab3ig  6964  suppimacnv  8153  odi  8543  nndi  8587  preleqALT  9570  inf3lem2  9582  pr2neOLD  9958  zorn2lem7  10455  uzind2  12627  ssfzo12  13720  elfznelfzo  13733  injresinj  13749  suppssfz  13959  sqlecan  14174  fi1uzind  14472  cramerimplem2  22571  fiinopn  22788  uhgr0v0e  29165  0uhgrsubgr  29206  0uhgrrusgr  29506  ewlkprop  29531  umgrwwlks2on  29887  3cyclfrgrrn1  30214  3cyclfrgrrn  30215  vdgn1frgrv2  30225  dvrunz  37948  ee223  44624  afveu  47154  afv2eu  47239  lindslinindsimp2  48452  nn0sumshdiglemB  48609