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  3301  rspc2gv  3319  intss1  4490  fvopab3ig  6276  suppimacnv  7303  odi  7656  nndi  7700  inf3lem2  8523  pr2ne  8825  zorn2lem7  9321  uzind2  11467  ssfzo12  12557  elfznelfzo  12569  injresinj  12584  suppssfz  12789  sqlecan  12966  fi1uzind  13274  fi1uzindOLD  13280  cramerimplem2  20484  fiinopn  20700  uhgr0v0e  26124  0uhgrsubgr  26165  0uhgrrusgr  26468  ewlkprop  26493  umgrwwlks2on  26844  3cyclfrgrrn1  27142  3cyclfrgrrn  27143  vdgn1frgrv2  27153  numclwlk1lem2foa  27208  dvrunz  33733  ee223  38685  afveu  41002  lindslinindsimp2  42023  nn0sumshdiglemB  42185