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  6977  suppimacnv  8169  odi  8565  nndi  8610  preleqALT  9596  inf3lem2  9608  zorn2lem7  10552  uzind2  12762  ssfzo12  13863  elfznelfzo  13877  injresinj  13895  suppssfz  14106  sqlecan  14321  fi1uzind  14620  cramerimplem2  22964  fiinopn  23181  uhgr0v0e  29753  0uhgrsubgr  29794  0uhgrrusgr  30093  ewlkprop  30118  usgrwwlks2on  30481  umgrwwlks2on  30482  3cyclfrgrrn1  30820  3cyclfrgrrn  30821  vdgn1frgrv2  30831  dvrunz  38808  ee223  45561  afveu  48145  afv2eu  48230  lindslinindsimp2  49497  nn0sumshdiglemB  49654