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  3595  rspc2gv  3617  intss1  4961  fvopab3ig  6995  suppimacnv  8172  odi  8593  nndi  8637  preleqALT  9632  inf3lem2  9644  pr2neOLD  10020  zorn2lem7  10517  uzind2  12677  ssfzo12  13749  elfznelfzo  13761  injresinj  13777  suppssfz  13983  sqlecan  14196  fi1uzind  14482  cramerimplem2  22573  fiinopn  22790  uhgr0v0e  29038  0uhgrsubgr  29079  0uhgrrusgr  29379  ewlkprop  29404  umgrwwlks2on  29755  3cyclfrgrrn1  30082  3cyclfrgrrn  30083  vdgn1frgrv2  30093  dvrunz  37362  ee223  43996  afveu  46456  afv2eu  46541  lindslinindsimp2  47454  nn0sumshdiglemB  47616