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  3599  rspc2gv  3620  intss1  4966  fvopab3ig  6993  suppimacnv  8161  odi  8581  nndi  8625  preleqALT  9614  inf3lem2  9626  pr2neOLD  10002  zorn2lem7  10499  uzind2  12659  ssfzo12  13729  elfznelfzo  13741  injresinj  13757  suppssfz  13963  sqlecan  14177  fi1uzind  14462  cramerimplem2  22406  fiinopn  22623  uhgr0v0e  28762  0uhgrsubgr  28803  0uhgrrusgr  29102  ewlkprop  29127  umgrwwlks2on  29478  3cyclfrgrrn1  29805  3cyclfrgrrn  29806  vdgn1frgrv2  29816  dvrunz  37125  ee223  43697  afveu  46159  afv2eu  46244  lindslinindsimp2  47231  nn0sumshdiglemB  47393