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  3564  rspc2gv  3585  intss1  4922  fvopab3ig  6989  suppimacnv  8192  odi  8588  nndi  8633  preleqALT  9619  inf3lem2  9631  zorn2lem7  10581  uzind2  12793  ssfzo12  13895  elfznelfzo  13909  injresinj  13927  suppssfz  14138  sqlecan  14354  fi1uzind  14653  cramerimplem2  23003  fiinopn  23220  uhgr0v0e  29820  0uhgrsubgr  29861  0uhgrrusgr  30160  ewlkprop  30185  usgrwwlks2on  30548  umgrwwlks2on  30549  3cyclfrgrrn1  30887  3cyclfrgrrn  30888  vdgn1frgrv2  30898  dvrunz  38964  ee223  45693  afveu  48299  afv2eu  48384  lindslinindsimp2  49651  nn0sumshdiglemB  49808