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  3590  intss1  4927  fvopab3ig  6985  suppimacnv  8168  odi  8562  nndi  8607  preleqALT  9584  inf3lem2  9596  zorn2lem7  10492  uzind2  12695  ssfzo12  13795  elfznelfzo  13809  injresinj  13827  suppssfz  14037  sqlecan  14252  fi1uzind  14551  cramerimplem2  22852  fiinopn  23069  uhgr0v0e  29599  0uhgrsubgr  29640  0uhgrrusgr  29939  ewlkprop  29964  usgrwwlks2on  30318  umgrwwlks2on  30319  3cyclfrgrrn1  30647  3cyclfrgrrn  30648  vdgn1frgrv2  30658  dvrunz  38633  ee223  45371  afveu  47918  afv2eu  48003  lindslinindsimp2  49271  nn0sumshdiglemB  49428