Theorem pm2.43a 55

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 23	. 2 ⊢ (𝜓 → 𝜓)
2		pm2.43a.1	. 2 ⊢ (𝜓 → (𝜑 → (𝜓 → 𝜒)))
3	1, 2	mpid 45	1 ⊢ (𝜓 → (𝜑 → 𝜒))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  pm2.43b  56  rspc  3567  rspc2gv  3589  intss1  4926  fvopab3ig  6986  suppimacnv  8175  odi  8569  nndi  8614  preleqALT  9599  inf3lem2  9611  zorn2lem7  10507  uzind2  12717  ssfzo12  13817  elfznelfzo  13831  injresinj  13849  suppssfz  14060  sqlecan  14275  fi1uzind  14574  cramerimplem2  22913  fiinopn  23130  uhgr0v0e  29699  0uhgrsubgr  29740  0uhgrrusgr  30039  ewlkprop  30064  usgrwwlks2on  30427  umgrwwlks2on  30428  3cyclfrgrrn1  30766  3cyclfrgrrn  30767  vdgn1frgrv2  30777  dvrunz  38706  ee223  45459  afveu  48043  afv2eu  48128  lindslinindsimp2  49395  nn0sumshdiglemB  49552