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  3562  rspc2gv  3584  intss1  4915  fvopab3ig  6934  suppimacnv  8113  odi  8503  nndi  8547  preleqALT  9517  inf3lem2  9529  zorn2lem7  10403  uzind2  12576  ssfzo12  13669  elfznelfzo  13683  injresinj  13701  suppssfz  13911  sqlecan  14126  fi1uzind  14424  cramerimplem2  22609  fiinopn  22826  uhgr0v0e  29227  0uhgrsubgr  29268  0uhgrrusgr  29568  ewlkprop  29593  usgrwwlks2on  29947  umgrwwlks2on  29948  3cyclfrgrrn1  30276  3cyclfrgrrn  30277  vdgn1frgrv2  30287  dvrunz  38004  ee223  44741  afveu  47267  afv2eu  47352  lindslinindsimp2  48578  nn0sumshdiglemB  48735