Theorem pm2.43a 54

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 22	. 2 ⊢ (𝜓 → 𝜓)
2		pm2.43a.1	. 2 ⊢ (𝜓 → (𝜑 → (𝜓 → 𝜒)))
3	1, 2	mpid 44	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  55  rspc  3564  rspc2gv  3586  intss1  4915  fvopab3ig  6960  suppimacnv  8142  odi  8536  nndi  8581  preleqALT  9562  inf3lem2  9574  zorn2lem7  10449  uzind2  12656  ssfzo12  13755  elfznelfzo  13769  injresinj  13787  suppssfz  13997  sqlecan  14212  fi1uzind  14510  cramerimplem2  22717  fiinopn  22934  uhgr0v0e  29378  0uhgrsubgr  29419  0uhgrrusgr  29718  ewlkprop  29743  usgrwwlks2on  30097  umgrwwlks2on  30098  3cyclfrgrrn1  30426  3cyclfrgrrn  30427  vdgn1frgrv2  30437  dvrunz  38401  ee223  45158  afveu  47695  afv2eu  47780  lindslinindsimp2  49033  nn0sumshdiglemB  49190