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  3303  rspc2gv  3321  intss1  4492  fvopab3ig  6278  suppimacnv  7306  odi  7659  nndi  7703  inf3lem2  8526  pr2ne  8828  zorn2lem7  9324  uzind2  11470  ssfzo12  12561  elfznelfzo  12573  injresinj  12589  suppssfz  12794  sqlecan  12971  fi1uzind  13279  fi1uzindOLD  13285  cramerimplem2  20490  fiinopn  20706  uhgr0v0e  26130  0uhgrsubgr  26171  0uhgrrusgr  26474  ewlkprop  26499  umgrwwlks2on  26850  3cyclfrgrrn1  27149  3cyclfrgrrn  27150  vdgn1frgrv2  27160  dvrunz  33753  ee223  38859  afveu  41233  lindslinindsimp2  42252  nn0sumshdiglemB  42414