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  3613  rspc2gv  3634  intss1  4893  fvopab3ig  6766  suppimacnv  7843  odi  8207  nndi  8251  preleqALT  9082  inf3lem2  9094  pr2ne  9433  zorn2lem7  9926  uzind2  12078  ssfzo12  13133  elfznelfzo  13145  injresinj  13161  suppssfz  13365  sqlecan  13574  fi1uzind  13858  cramerimplem2  21295  fiinopn  21511  uhgr0v0e  27022  0uhgrsubgr  27063  0uhgrrusgr  27362  ewlkprop  27387  umgrwwlks2on  27738  3cyclfrgrrn1  28066  3cyclfrgrrn  28067  vdgn1frgrv2  28077  dvrunz  35234  ee223  40975  afveu  43359  afv2eu  43444  lindslinindsimp2  44525  nn0sumshdiglemB  44687