Theorem pm2.43a 52

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 43	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  53  rspc  3276  intss1  4427  fvopab3ig  6188  suppimacnv  7193  odi  7546  nndi  7590  inf3lem2  8409  pr2ne  8711  zorn2lem7  9207  uzind2  11346  ssfzo12  12427  elfznelfzo  12439  injresinj  12451  suppssfz  12656  sqlecan  12833  fi1uzind  13134  fi1uzindOLD  13140  cramerimplem2  20309  fiinopn  20531  usgraedg4  25916  wlkdvspthlem  26137  usgrcyclnl1  26168  3cyclfrgrarn1  26539  vdn0frgrav2  26550  vdn1frgrav2  26552  vdgn1frgrav2  26553  numclwlk1lem2foa  26618  dvrunz  32923  ee223  37880  afveu  39882  uhgr0v0e  40464  0uhgrsubgr  40503  0uhgrrusgr  40778  ewlkprop  40805  umgrwwlks2on  41161  3cyclfrgrrn1  41455  3cyclfrgrrn  41456  vdgn1frgrv2  41466  av-numclwlk1lem2foa  41521  lindslinindsimp2  42046  nn0sumshdiglemB  42212