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  1055  sbc2or  3750  eq0rdvALT  4361  rzalALT  4449  reusv2lem2  5345  po2ne  5549  poirr2  6082  sofld  6146  dfwe2  7721  tfindsg  7805  findsg  7841  omopth2  8513  swoord2  8671  unxpdomlem3  9162  preleqg  9528  suc11reg  9532  wemapwe  9610  r111  9691  r1pwss  9700  cflim2  10177  axunndlem1  10510  axunnd  10511  axpowndlem3  10514  axpownd  10516  axregndlem1  10517  axregndlem2  10518  axinfndlem1  10520  axinfnd  10521  axacndlem1  10522  axacndlem2  10523  axacndlem3  10524  axacndlem4  10525  axacndlem5  10526  axacnd  10527  fpwwe2lem12  10557  gchpwdom  10585  winalim2  10611  ltapr  10960  prodgt0  11992  squeeze0  12049  nnsub  12193  nn0sub  12455  elnnz  12502  nn0lt10b  12558  indstr2  12844  uzsupss  12857  nn01to3  12858  xrltnsym  13055  xrlttr  13058  qbtwnxr  13119  xltnegi  13135  xmullem  13183  xlemul1a  13207  xrsupsslem  13226  xrinfmsslem  13227  xrub  13231  xrsup0  13242  xrinf0  13258  reltxrnmnf  13262  ixxdisj  13280  icodisj  13396  fzm1  13527  addmodlteq  13873  facdiv  14214  hasheqf1oi  14278  relexpfld  14976  relexpuzrel  14979  reusq0  15392  climuni  15479  rlimno1  15581  sqrt2irr  16178  nn0rppwr  16492  prmdvdsexpr  16648  prmfac1  16651  dvdsprmpweqle  16818  ramlb  16951  ram0  16954  prmgaplem6  16988  prmlem1  17039  prmlem2  17051  pospo  18270  efgredlemc  19678  efgred  19681  ablsimpnosubgd  20039  sdrgacs  20738  prmirred  21433  psrvscafval  21908  fvmptnn04ifa  22798  fvmptnn04ifb  22799  fvmptnn04ifc  22800  fvmptnn04ifd  22801  chfacfscmulgsum  22808  chfacfpmmulgsum  22812  0top  22931  pnfnei  23168  mnfnei  23169  cmpfi  23356  1stccnp  23410  filconn  23831  ivthlem2  25413  ivthlem3  25414  ovolicc2lem3  25480  itg1addlem4  25660  itg2seq  25703  dvcnvlem  25940  lhop2  25980  bpos1  27254  lgsdir2lem2  27297  lgsqrlem2  27318  lgseisenlem2  27347  2sqnn  27410  pntlem3  27580  ostth3  27609  nosupbnd1lem5  27684  noinfbnd1lem5  27699  noetasuplem4  27708  noetainflem4  27712  elnnzs  28380  expsne0  28415  tgcgr4  28586  axlowdimlem15  29012  nbusgrvtxm1  29435  wlkv0  29706  1to2vfriswmgr  30337  n4cyclfrgr  30349  frgrnbnb  30351  frgrregord013  30453  snsssng  32571  ifeqeqx  32599  rprmdvdsprod  33596  fldext2chn  33866  f1resrcmplf1dlem  35223  erdszelem4  35369  erdszelem8  35373  antnestlaw3lem  35865  finminlem  36493  nn0prpwlem  36497  nn0prpw  36498  ordcmp  36622  iooelexlt  37538  relowlssretop  37539  smprngopr  38224  disjlem14  39073  prtlem14  39171  atltcvr  39732  dihord6apre  41553  dihord6b  41557  jm2.23  43274  onexlimgt  43521  ordnexbtwnsuc  43545  onov0suclim  43552  relexpmulg  43987  rzalf  45298  or2expropbi  47316  icceuelpart  47718  iccpartnel  47720  poprelb  47806  goldbachthlem2  47828  fmtnoprmfac1  47847  fmtnoprmfac2  47849  fmtno4prmfac  47854  fmtno4prmfac193  47855  2pwp1prm  47871  lighneallem4  47892  requad1  47904  requad2  47905  evenprm2  47996  odd2prm2  48000  stgoldbwt  48058  sbgoldbwt  48059  sbgoldbalt  48063  usgrexmpl12ngric  48320  pgnbgreunbgrlem2  48399  pgnbgreunbgrlem5  48405  ztprmneprm  48629  functermc  49789