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  3610  rspc2gv  3632  intss1  4963  fvopab3ig  7012  suppimacnv  8199  odi  8617  nndi  8661  preleqALT  9657  inf3lem2  9669  pr2neOLD  10045  zorn2lem7  10542  uzind2  12711  ssfzo12  13798  elfznelfzo  13811  injresinj  13827  suppssfz  14035  sqlecan  14248  fi1uzind  14546  cramerimplem2  22690  fiinopn  22907  uhgr0v0e  29255  0uhgrsubgr  29296  0uhgrrusgr  29596  ewlkprop  29621  umgrwwlks2on  29977  3cyclfrgrrn1  30304  3cyclfrgrrn  30305  vdgn1frgrv2  30315  dvrunz  37961  ee223  44654  afveu  47165  afv2eu  47250  lindslinindsimp2  48380  nn0sumshdiglemB  48541