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  prlem1  1054  sbc2or  3753  eq0rdvALT  4361  rzalALT  4463  reusv2lem2  5341  po2ne  5547  poirr2  6077  sofld  6140  dfwe2  7714  tfindsg  7801  findsg  7837  omopth2  8509  swoord2  8665  unxpdomlem3  9157  preleqg  9530  suc11reg  9534  wemapwe  9612  r111  9690  r1pwss  9699  cflim2  10176  axunndlem1  10508  axunnd  10509  axpowndlem3  10512  axpownd  10514  axregndlem1  10515  axregndlem2  10516  axinfndlem1  10518  axinfnd  10519  axacndlem1  10520  axacndlem2  10521  axacndlem3  10522  axacndlem4  10523  axacndlem5  10524  axacnd  10525  fpwwe2lem12  10555  gchpwdom  10583  winalim2  10609  ltapr  10958  prodgt0  11989  squeeze0  12046  nnsub  12190  nn0sub  12452  elnnz  12499  nn0lt10b  12556  indstr2  12846  uzsupss  12859  nn01to3  12860  xrltnsym  13057  xrlttr  13060  qbtwnxr  13120  xltnegi  13136  xmullem  13184  xlemul1a  13208  xrsupsslem  13227  xrinfmsslem  13228  xrub  13232  xrsup0  13243  xrinf0  13259  reltxrnmnf  13263  ixxdisj  13281  icodisj  13397  fzm1  13528  addmodlteq  13871  facdiv  14212  hasheqf1oi  14276  relexpfld  14974  relexpuzrel  14977  reusq0  15390  climuni  15477  rlimno1  15579  sqrt2irr  16176  nn0rppwr  16490  prmdvdsexpr  16646  prmfac1  16649  dvdsprmpweqle  16816  ramlb  16949  ram0  16952  prmgaplem6  16986  prmlem1  17037  prmlem2  17049  pospo  18267  efgredlemc  19642  efgred  19645  ablsimpnosubgd  20003  sdrgacs  20704  prmirred  21399  psrvscafval  21873  fvmptnn04ifa  22753  fvmptnn04ifb  22754  fvmptnn04ifc  22755  fvmptnn04ifd  22756  chfacfscmulgsum  22763  chfacfpmmulgsum  22767  0top  22886  pnfnei  23123  mnfnei  23124  cmpfi  23311  1stccnp  23365  filconn  23786  ivthlem2  25369  ivthlem3  25370  ovolicc2lem3  25436  itg1addlem4  25616  itg2seq  25659  dvcnvlem  25896  lhop2  25936  bpos1  27210  lgsdir2lem2  27253  lgsqrlem2  27274  lgseisenlem2  27303  2sqnn  27366  pntlem3  27536  ostth3  27565  nosupbnd1lem5  27640  noinfbnd1lem5  27655  noetasuplem4  27664  noetainflem4  27668  elnnzs  28312  expsne0  28346  tgcgr4  28494  axlowdimlem15  28919  nbusgrvtxm1  29342  wlkv0  29613  1to2vfriswmgr  30241  n4cyclfrgr  30253  frgrnbnb  30255  frgrregord013  30357  snsssng  32476  ifeqeqx  32504  rprmdvdsprod  33481  fldext2chn  33694  f1resrcmplf1dlem  35052  erdszelem4  35166  erdszelem8  35170  antnestlaw3lem  35662  finminlem  36291  nn0prpwlem  36295  nn0prpw  36296  ordcmp  36420  iooelexlt  37335  relowlssretop  37336  smprngopr  38031  disjlem14  38775  prtlem14  38852  atltcvr  39414  dihord6apre  41235  dihord6b  41239  jm2.23  42969  onexlimgt  43216  ordnexbtwnsuc  43240  onov0suclim  43247  relexpmulg  43683  rzalf  44995  or2expropbi  47019  icceuelpart  47421  iccpartnel  47423  poprelb  47509  goldbachthlem2  47531  fmtnoprmfac1  47550  fmtnoprmfac2  47552  fmtno4prmfac  47557  fmtno4prmfac193  47558  2pwp1prm  47574  lighneallem4  47595  requad1  47607  requad2  47608  evenprm2  47699  odd2prm2  47703  stgoldbwt  47761  sbgoldbwt  47762  sbgoldbalt  47766  usgrexmpl12ngric  48013  pgnbgreunbgrlem2  48091  pgnbgreunbgrlem5  48097  ztprmneprm  48319  functermc  49481