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  3549  rspc2gv  3569  intss1  4894  fvopab3ig  6871  suppimacnv  7990  odi  8410  nndi  8454  preleqALT  9375  inf3lem2  9387  pr2ne  9761  zorn2lem7  10258  uzind2  12413  ssfzo12  13480  elfznelfzo  13492  injresinj  13508  suppssfz  13714  sqlecan  13925  fi1uzind  14211  cramerimplem2  21833  fiinopn  22050  uhgr0v0e  27605  0uhgrsubgr  27646  0uhgrrusgr  27945  ewlkprop  27970  umgrwwlks2on  28322  3cyclfrgrrn1  28649  3cyclfrgrrn  28650  vdgn1frgrv2  28660  dvrunz  36112  ee223  42254  afveu  44645  afv2eu  44730  lindslinindsimp2  45804  nn0sumshdiglemB  45966