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  3797  eq0rdvALT  4408  rzalALT  4510  reusv2lem2  5399  po2ne  5608  poirr2  6144  sofld  6207  dfwe2  7794  tfindsg  7882  findsg  7919  omopth2  8622  swoord2  8778  unxpdomlem3  9288  preleqg  9655  suc11reg  9659  wemapwe  9737  r111  9815  r1pwss  9824  cflim2  10303  axunndlem1  10635  axunnd  10636  axpowndlem3  10639  axpownd  10641  axregndlem1  10642  axregndlem2  10643  axinfndlem1  10645  axinfnd  10646  axacndlem1  10647  axacndlem2  10648  axacndlem3  10649  axacndlem4  10650  axacndlem5  10651  axacnd  10652  fpwwe2lem12  10682  gchpwdom  10710  winalim2  10736  ltapr  11085  prodgt0  12114  squeeze0  12171  nnsub  12310  nn0sub  12576  elnnz  12623  nn0lt10b  12680  indstr2  12969  uzsupss  12982  nn01to3  12983  xrltnsym  13179  xrlttr  13182  qbtwnxr  13242  xltnegi  13258  xmullem  13306  xlemul1a  13330  xrsupsslem  13349  xrinfmsslem  13350  xrub  13354  xrsup0  13365  xrinf0  13380  reltxrnmnf  13384  ixxdisj  13402  icodisj  13516  fzm1  13647  addmodlteq  13987  facdiv  14326  hasheqf1oi  14390  relexpfld  15088  relexpuzrel  15091  reusq0  15501  climuni  15588  rlimno1  15690  sqrt2irr  16285  nn0rppwr  16598  prmdvdsexpr  16754  prmfac1  16757  dvdsprmpweqle  16924  ramlb  17057  ram0  17060  prmgaplem6  17094  prmlem1  17145  prmlem2  17157  pospo  18390  efgredlemc  19763  efgred  19766  ablsimpnosubgd  20124  sdrgacs  20802  prmirred  21485  psrvscafval  21968  fvmptnn04ifa  22856  fvmptnn04ifb  22857  fvmptnn04ifc  22858  fvmptnn04ifd  22859  chfacfscmulgsum  22866  chfacfpmmulgsum  22870  0top  22990  pnfnei  23228  mnfnei  23229  cmpfi  23416  1stccnp  23470  filconn  23891  ivthlem2  25487  ivthlem3  25488  ovolicc2lem3  25554  itg1addlem4  25734  itg2seq  25777  dvcnvlem  26014  lhop2  26054  bpos1  27327  lgsdir2lem2  27370  lgsqrlem2  27391  lgseisenlem2  27420  2sqnn  27483  pntlem3  27653  ostth3  27682  nosupbnd1lem5  27757  noinfbnd1lem5  27772  noetasuplem4  27781  noetainflem4  27785  elnnzs  28387  expsne0  28414  tgcgr4  28539  axlowdimlem15  28971  nbusgrvtxm1  29396  wlkv0  29669  1to2vfriswmgr  30298  n4cyclfrgr  30310  frgrnbnb  30312  frgrregord013  30414  snsssng  32533  ifeqeqx  32555  rprmdvdsprod  33562  fldext2chn  33769  f1resrcmplf1dlem  35100  erdszelem4  35199  erdszelem8  35203  finminlem  36319  nn0prpwlem  36323  nn0prpw  36324  ordcmp  36448  iooelexlt  37363  relowlssretop  37364  smprngopr  38059  disjlem14  38799  prtlem14  38875  atltcvr  39437  dihord6apre  41258  dihord6b  41262  jm2.23  43008  onexlimgt  43255  ordnexbtwnsuc  43280  onov0suclim  43287  relexpmulg  43723  rzalf  45022  or2expropbi  47046  icceuelpart  47423  iccpartnel  47425  poprelb  47511  goldbachthlem2  47533  fmtnoprmfac1  47552  fmtnoprmfac2  47554  fmtno4prmfac  47559  fmtno4prmfac193  47560  2pwp1prm  47576  lighneallem4  47597  requad1  47609  requad2  47610  evenprm2  47701  odd2prm2  47705  stgoldbwt  47763  sbgoldbwt  47764  sbgoldbalt  47768  usgrexmpl12ngric  47997  ztprmneprm  48263  functermc  49140