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  3566  rspc2gv  3588  intss1  4920  fvopab3ig  6945  suppimacnv  8126  odi  8516  nndi  8561  preleqALT  9538  inf3lem2  9550  zorn2lem7  10424  uzind2  12597  ssfzo12  13687  elfznelfzo  13701  injresinj  13719  suppssfz  13929  sqlecan  14144  fi1uzind  14442  cramerimplem2  22640  fiinopn  22857  uhgr0v0e  29323  0uhgrsubgr  29364  0uhgrrusgr  29664  ewlkprop  29689  usgrwwlks2on  30043  umgrwwlks2on  30044  3cyclfrgrrn1  30372  3cyclfrgrrn  30373  vdgn1frgrv2  30383  dvrunz  38194  ee223  44979  afveu  47502  afv2eu  47587  lindslinindsimp2  48812  nn0sumshdiglemB  48969