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  3553  rspc2gv  3575  intss1  4906  fvopab3ig  6944  suppimacnv  8124  odi  8514  nndi  8559  preleqALT  9538  inf3lem2  9550  zorn2lem7  10424  uzind2  12622  ssfzo12  13714  elfznelfzo  13728  injresinj  13746  suppssfz  13956  sqlecan  14171  fi1uzind  14469  cramerimplem2  22649  fiinopn  22866  uhgr0v0e  29307  0uhgrsubgr  29348  0uhgrrusgr  29647  ewlkprop  29672  usgrwwlks2on  30026  umgrwwlks2on  30027  3cyclfrgrrn1  30355  3cyclfrgrrn  30356  vdgn1frgrv2  30366  dvrunz  38275  ee223  45061  afveu  47595  afv2eu  47680  lindslinindsimp2  48933  nn0sumshdiglemB  49090