Theorem pm2.21d 619

Description: A contradiction implies anything. Deduction from pm2.21 617. (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 617	. 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 615

This theorem is referenced by:  pm2.21dd  620  pm5.21  695  2falsed  702  mtord  783  prlem1  973  eq0rdv  3467  csbprc  3468  rzal  3520  poirr2  5018  nnsucuniel  6491  nnawordex  6525  swoord2  6560  difinfsnlem  7093  exmidomni  7135  elni2  7308  cauappcvgprlemdisj  7645  caucvgprlemdisj  7668  caucvgprprlemdisj  7696  caucvgsr  7796  lelttr  8040  nnsub  8952  nn0ge2m1nn  9230  elnnz  9257  elnn0z  9260  indstr  9587  indstr2  9603  xrltnsym  9787  xrlttr  9789  xrltso  9790  xrlelttr  9800  xltnegi  9829  xsubge0  9875  ixxdisj  9897  icodisj  9986  fzm1  10093  qbtwnxr  10251  frec2uzlt2d  10397  nn0ltexp2  10681  facdiv  10709  resqrexlemgt0  11020  climuni  11292  fsumcl2lem  11397  dvdsle  11840  prmdvdsexpr  12140  prmfac1  12142  sqrt2irr  12152  phibndlem  12206  dvdsprmpweqle  12326  isxmet2d  13630  lgsdir2lem2  14212  trilpolemres  14561