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  5021  nnsucuniel  6495  nnawordex  6529  swoord2  6564  difinfsnlem  7097  exmidomni  7139  elni2  7312  cauappcvgprlemdisj  7649  caucvgprlemdisj  7672  caucvgprprlemdisj  7700  caucvgsr  7800  lelttr  8045  nnsub  8957  nn0ge2m1nn  9235  elnnz  9262  elnn0z  9265  indstr  9592  indstr2  9608  xrltnsym  9792  xrlttr  9794  xrltso  9795  xrlelttr  9805  xltnegi  9834  xsubge0  9880  ixxdisj  9902  icodisj  9991  fzm1  10099  qbtwnxr  10257  frec2uzlt2d  10403  nn0ltexp2  10688  facdiv  10717  resqrexlemgt0  11028  climuni  11300  fsumcl2lem  11405  dvdsle  11849  prmdvdsexpr  12149  prmfac1  12151  sqrt2irr  12161  phibndlem  12215  dvdsprmpweqle  12335  isxmet2d  13818  lgsdir2lem2  14400  lgseisenlem2  14421  trilpolemres  14760