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  3568  rspc2gv  3589  intss1  4926  fvopab3ig  7012  suppimacnv  8219  odi  8615  nndi  8660  preleqALT  9645  inf3lem2  9657  zorn2lem7  10607  uzind2  12819  ssfzo12  13921  elfznelfzo  13935  injresinj  13953  suppssfz  14164  sqlecan  14380  fi1uzind  14679  cramerimplem2  23032  fiinopn  23249  uhgr0v0e  29849  0uhgrsubgr  29890  0uhgrrusgr  30189  ewlkprop  30214  usgrwwlks2on  30577  umgrwwlks2on  30578  3cyclfrgrrn1  30916  3cyclfrgrrn  30917  vdgn1frgrv2  30927  dvrunz  39080  ee223  45808  afveu  48428  afv2eu  48513  lindslinindsimp2  49780  nn0sumshdiglemB  49937