Theorem pm2.21d 119

Description: A contradiction implies anything. Deduction associated with pm2.21 121. (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	. . 3 ⊢ (𝜑 → ¬ 𝜓)
2	1	a1d 25	. 2 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))
3	2	con4d 115	1 ⊢ (𝜑 → (𝜓 → 𝜒))

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by:  pm2.21ddALT  120  pm2.21  121  2falsed  369  pm5.14  929  ecase2d  1012  prlem1  1035  sbc2or  3686  eq0rdv  4237  rzal  4330  reusv2lem2  5147  po2ne  5334  poirr2  5818  sofld  5878  dfwe2  7306  tfindsg  7385  findsg  7418  omopth2  8003  swoord2  8113  unxpdomlem3  8511  preleqg  8864  suc11reg  8868  wemapwe  8946  r111  8990  r1pwss  8999  cflim2  9475  axunndlem1  9807  axunnd  9808  axpowndlem3  9811  axpownd  9813  axregndlem1  9814  axregndlem2  9815  axinfndlem1  9817  axinfnd  9818  axacndlem1  9819  axacndlem2  9820  axacndlem3  9821  axacndlem4  9822  axacndlem5  9823  axacnd  9824  fpwwe2lem13  9854  gchpwdom  9882  winalim2  9908  ltapr  10257  prodgt0  11280  squeeze0  11336  nnsub  11477  nn0sub  11752  elnnz  11796  nn0lt10b  11850  indstr2  12134  uzsupss  12147  nn01to3  12148  xrltnsym  12340  xrlttr  12343  qbtwnxr  12403  xltnegi  12419  xmullem  12466  xlemul1a  12490  xrsupsslem  12509  xrinfmsslem  12510  xrub  12514  xrsup0  12525  xrinf0  12540  reltxrnmnf  12544  ixxdisj  12562  icodisj  12671  fzm1  12796  addmodlteq  13122  facdiv  13455  hasheqf1oi  13520  relexpfld  14259  relexpuzrel  14262  reusq0  14673  climuni  14760  rlimno1  14861  sqrt2irr  15452  prmdvdsexpr  15907  prmfac1  15909  dvdsprmpweqle  16068  ramlb  16201  ram0  16204  prmgaplem6  16238  prmlem1  16287  prmlem2  16299  pospo  17431  symgbas  18259  efgredlemc  18620  efgred  18624  sdrgacs  19292  psrvscafval  19874  prmirred  20334  fvmptnn04ifa  21152  fvmptnn04ifb  21153  fvmptnn04ifc  21154  fvmptnn04ifd  21155  chfacfscmulgsum  21162  chfacfpmmulgsum  21166  0top  21285  pnfnei  21522  mnfnei  21523  cmpfi  21710  1stccnp  21764  filconn  22185  ivthlem2  23746  ivthlem3  23747  ovolicc2lem3  23813  itg1addlem4  23993  itg2seq  24036  dvcnvlem  24266  lhop2  24305  bpos1  25551  lgsdir2lem2  25594  lgsqrlem2  25615  lgseisenlem2  25644  2sqnn  25707  pntlem3  25877  ostth3  25906  tgcgr4  26009  axlowdimlem15  26435  nbusgrvtxm1  26854  wlkv0  27125  1to2vfriswmgr  27803  n4cyclfrgr  27815  frgrnbnb  27817  frgrregord013  27942  ifeqeqx  30055  erdszelem4  31986  erdszelem8  31990  nosupbnd1lem5  32673  noetalem3  32680  finminlem  33127  nn0prpwlem  33131  nn0prpw  33132  ordcmp  33255  iooelexlt  34020  relowlssretop  34021  smprngopr  34720  prtlem14  35403  atltcvr  35964  dihord6apre  37785  dihord6b  37789  nn0rppwr  38559  jm2.23  38934  rp-fakeimass  39219  relexpmulg  39363  ablsimpnosubgd  39985  rzalf  40637  or2expropbi  42620  icceuelpart  42914  iccpartnel  42916  poprelb  42994  goldbachthlem2  43016  fmtnoprmfac1  43035  fmtnoprmfac2  43037  fmtno4prmfac  43042  fmtno4prmfac193  43043  2pwp1prm  43059  lighneallem4  43083  requad1  43095  requad2  43096  evenprm2  43187  odd2prm2  43191  stgoldbwt  43249  sbgoldbwt  43250  sbgoldbalt  43254  ztprmneprm  43699