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  3539  rspc2gv  3561  intss1  4891  fvopab3ig  6853  suppimacnv  7961  odi  8372  nndi  8416  preleqALT  9305  inf3lem2  9317  pr2ne  9692  zorn2lem7  10189  uzind2  12343  ssfzo12  13408  elfznelfzo  13420  injresinj  13436  suppssfz  13642  sqlecan  13853  fi1uzind  14139  cramerimplem2  21741  fiinopn  21958  uhgr0v0e  27508  0uhgrsubgr  27549  0uhgrrusgr  27848  ewlkprop  27873  umgrwwlks2on  28223  3cyclfrgrrn1  28550  3cyclfrgrrn  28551  vdgn1frgrv2  28561  dvrunz  36039  ee223  42143  afveu  44532  afv2eu  44617  lindslinindsimp2  45692  nn0sumshdiglemB  45854