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  3579  rspc2gv  3601  intss1  4930  fvopab3ig  6967  suppimacnv  8156  odi  8546  nndi  8590  preleqALT  9577  inf3lem2  9589  pr2neOLD  9965  zorn2lem7  10462  uzind2  12634  ssfzo12  13727  elfznelfzo  13740  injresinj  13756  suppssfz  13966  sqlecan  14181  fi1uzind  14479  cramerimplem2  22578  fiinopn  22795  uhgr0v0e  29172  0uhgrsubgr  29213  0uhgrrusgr  29513  ewlkprop  29538  umgrwwlks2on  29894  3cyclfrgrrn1  30221  3cyclfrgrrn  30222  vdgn1frgrv2  30232  dvrunz  37955  ee223  44631  afveu  47158  afv2eu  47243  lindslinindsimp2  48456  nn0sumshdiglemB  48613