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 ⊢ (𝜓 → (𝜑 → 𝜒))

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  56  rspc  3572  rspc2gv  3594  intss1  4924  fvopab3ig  6975  suppimacnv  8158  odi  8552  nndi  8597  preleqALT  9574  inf3lem2  9586  zorn2lem7  10474  uzind2  12680  ssfzo12  13779  elfznelfzo  13793  injresinj  13811  suppssfz  14021  sqlecan  14236  fi1uzind  14534  cramerimplem2  22802  fiinopn  23019  uhgr0v0e  29497  0uhgrsubgr  29538  0uhgrrusgr  29837  ewlkprop  29862  usgrwwlks2on  30216  umgrwwlks2on  30217  3cyclfrgrrn1  30545  3cyclfrgrrn  30546  vdgn1frgrv2  30556  dvrunz  38465  ee223  45208  afveu  47745  afv2eu  47830  lindslinindsimp2  49094  nn0sumshdiglemB  49251