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  3568  rspc2gv  3590  intss1  4927  fvopab3ig  6985  suppimacnv  8169  odi  8563  nndi  8608  preleqALT  9585  inf3lem2  9597  zorn2lem7  10485  uzind2  12688  ssfzo12  13788  elfznelfzo  13802  injresinj  13820  suppssfz  14030  sqlecan  14245  fi1uzind  14544  cramerimplem2  22820  fiinopn  23037  uhgr0v0e  29554  0uhgrsubgr  29595  0uhgrrusgr  29894  ewlkprop  29919  usgrwwlks2on  30273  umgrwwlks2on  30274  3cyclfrgrrn1  30602  3cyclfrgrrn  30603  vdgn1frgrv2  30613  dvrunz  38571  ee223  45313  afveu  47857  afv2eu  47942  lindslinindsimp2  49210  nn0sumshdiglemB  49367