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  3600  rspc2gv  3620  intss1  4966  fvopab3ig  6991  suppimacnv  8155  odi  8575  nndi  8619  preleqALT  9608  inf3lem2  9620  pr2neOLD  9996  zorn2lem7  10493  uzind2  12651  ssfzo12  13721  elfznelfzo  13733  injresinj  13749  suppssfz  13955  sqlecan  14169  fi1uzind  14454  cramerimplem2  22177  fiinopn  22394  uhgr0v0e  28484  0uhgrsubgr  28525  0uhgrrusgr  28824  ewlkprop  28849  umgrwwlks2on  29200  3cyclfrgrrn1  29527  3cyclfrgrrn  29528  vdgn1frgrv2  29538  dvrunz  36810  ee223  43380  afveu  45847  afv2eu  45932  lindslinindsimp2  47097  nn0sumshdiglemB  47259