Theorem pm2.21d 121

Description: A contradiction implies anything. Deduction associated with pm2.21 123. (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  122  pm2.21  123  pm2.521g  174  2falsedOLD  377  ecase2dOLD  1029  prlem1  1053  sbc2or  3751  eq0rdvALT  4370  rzalALT  4472  reusv2lem2  5359  po2ne  5566  poirr2  6083  sofld  6144  dfwe2  7713  tfindsg  7802  findsg  7841  omopth2  8536  swoord2  8687  unxpdomlem3  9203  preleqg  9560  suc11reg  9564  wemapwe  9642  r111  9720  r1pwss  9729  cflim2  10208  axunndlem1  10540  axunnd  10541  axpowndlem3  10544  axpownd  10546  axregndlem1  10547  axregndlem2  10548  axinfndlem1  10550  axinfnd  10551  axacndlem1  10552  axacndlem2  10553  axacndlem3  10554  axacndlem4  10555  axacndlem5  10556  axacnd  10557  fpwwe2lem12  10587  gchpwdom  10615  winalim2  10641  ltapr  10990  prodgt0  12011  squeeze0  12067  nnsub  12206  nn0sub  12472  elnnz  12518  nn0lt10b  12574  indstr2  12861  uzsupss  12874  nn01to3  12875  xrltnsym  13066  xrlttr  13069  qbtwnxr  13129  xltnegi  13145  xmullem  13193  xlemul1a  13217  xrsupsslem  13236  xrinfmsslem  13237  xrub  13241  xrsup0  13252  xrinf0  13267  reltxrnmnf  13271  ixxdisj  13289  icodisj  13403  fzm1  13531  addmodlteq  13861  facdiv  14197  hasheqf1oi  14261  relexpfld  14946  relexpuzrel  14949  reusq0  15359  climuni  15446  rlimno1  15550  sqrt2irr  16142  prmdvdsexpr  16604  prmfac1  16608  dvdsprmpweqle  16769  ramlb  16902  ram0  16905  prmgaplem6  16939  prmlem1  16991  prmlem2  17003  pospo  18248  efgredlemc  19541  efgred  19544  ablsimpnosubgd  19897  sdrgacs  20324  prmirred  20932  psrvscafval  21395  fvmptnn04ifa  22236  fvmptnn04ifb  22237  fvmptnn04ifc  22238  fvmptnn04ifd  22239  chfacfscmulgsum  22246  chfacfpmmulgsum  22250  0top  22370  pnfnei  22608  mnfnei  22609  cmpfi  22796  1stccnp  22850  filconn  23271  ivthlem2  24853  ivthlem3  24854  ovolicc2lem3  24920  itg1addlem4  25100  itg1addlem4OLD  25101  itg2seq  25144  dvcnvlem  25377  lhop2  25416  bpos1  26668  lgsdir2lem2  26711  lgsqrlem2  26732  lgseisenlem2  26761  2sqnn  26824  pntlem3  26994  ostth3  27023  nosupbnd1lem5  27097  noinfbnd1lem5  27112  noetasuplem4  27121  noetainflem4  27125  tgcgr4  27536  axlowdimlem15  27968  nbusgrvtxm1  28390  wlkv0  28662  1to2vfriswmgr  29286  n4cyclfrgr  29298  frgrnbnb  29300  frgrregord013  29402  snsssng  31505  ifeqeqx  31528  f1resrcmplf1dlem  33779  erdszelem4  33875  erdszelem8  33879  finminlem  34866  nn0prpwlem  34870  nn0prpw  34871  ordcmp  34995  iooelexlt  35906  relowlssretop  35907  smprngopr  36584  disjlem14  37333  prtlem14  37409  atltcvr  37971  dihord6apre  39792  dihord6b  39796  nn0rppwr  40877  jm2.23  41378  onexlimgt  41635  ordnexbtwnsuc  41660  onov0suclim  41667  relexpmulg  42104  rzalf  43344  or2expropbi  45388  icceuelpart  45748  iccpartnel  45750  poprelb  45836  goldbachthlem2  45858  fmtnoprmfac1  45877  fmtnoprmfac2  45879  fmtno4prmfac  45884  fmtno4prmfac193  45885  2pwp1prm  45901  lighneallem4  45922  requad1  45934  requad2  45935  evenprm2  46026  odd2prm2  46030  stgoldbwt  46088  sbgoldbwt  46089  sbgoldbalt  46093  ztprmneprm  46543