Theorem pm2.21d 624

Description: A contradiction implies anything. Deduction from pm2.21 622. (Contributed by NM, 10-Feb-1996.)

Hypothesis

Ref	Expression
pm2.21d.1	⊢ (𝜑 → ¬ 𝜓)

Assertion

Ref	Expression
pm2.21d	⊢ (𝜑 → (𝜓 → 𝜒))

Proof of Theorem pm2.21d

Step	Hyp	Ref	Expression
1		pm2.21d.1	. 2 ⊢ (𝜑 → ¬ 𝜓)
2		pm2.21 622	. 2 ⊢ (¬ 𝜓 → (𝜓 → 𝜒))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝜓 → 𝜒))

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in2 620

This theorem is referenced by:  pm2.21dd  625  pm5.21  702  2falsed  709  mtord  790  prlem1  981  eq0rdv  3539  csbprc  3540  rzal  3592  poirr2  5129  nnsucuniel  6663  nnawordex  6697  swoord2  6732  difinfsnlem  7298  exmidomni  7341  elni2  7534  cauappcvgprlemdisj  7871  caucvgprlemdisj  7894  caucvgprprlemdisj  7922  caucvgsr  8022  lelttr  8268  nnsub  9182  nn0ge2m1nn  9462  elnnz  9489  elnn0z  9492  indstr  9827  indstr2  9843  xrltnsym  10028  xrlttr  10030  xrltso  10031  xrlelttr  10041  xltnegi  10070  xsubge0  10116  ixxdisj  10138  icodisj  10227  fzm1  10335  qbtwnxr  10518  frec2uzlt2d  10667  nn0ltexp2  10972  facdiv  11001  resqrexlemgt0  11582  climuni  11855  fsumcl2lem  11961  dvdsle  12407  prmdvdsexpr  12724  prmfac1  12726  sqrt2irr  12736  phibndlem  12790  dvdsprmpweqle  12912  isxmet2d  15075  lgsdir2lem2  15761  lgseisenlem2  15803  wlkv0  16223  trilpolemres  16667