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  3738  eq0rdvALT  4349  rzalALT  4436  reusv2lem2  5334  po2ne  5546  poirr2  6079  sofld  6143  dfwe2  7719  tfindsg  7803  findsg  7839  omopth2  8510  swoord2  8668  unxpdomlem3  9159  preleqg  9525  suc11reg  9529  wemapwe  9607  r111  9688  r1pwss  9697  cflim2  10174  axunndlem1  10507  axunnd  10508  axpowndlem3  10511  axpownd  10513  axregndlem1  10514  axregndlem2  10515  axinfndlem1  10517  axinfnd  10518  axacndlem1  10519  axacndlem2  10520  axacndlem3  10521  axacndlem4  10522  axacndlem5  10523  axacnd  10524  fpwwe2lem12  10554  gchpwdom  10582  winalim2  10608  ltapr  10957  prodgt0  11991  squeeze0  12048  nnsub  12210  nn0sub  12476  elnnz  12523  nn0lt10b  12580  indstr2  12866  uzsupss  12879  nn01to3  12880  xrltnsym  13077  xrlttr  13080  qbtwnxr  13141  xltnegi  13157  xmullem  13205  xlemul1a  13229  xrsupsslem  13248  xrinfmsslem  13249  xrub  13253  xrsup0  13264  xrinf0  13280  reltxrnmnf  13284  ixxdisj  13302  icodisj  13418  fzm1  13550  addmodlteq  13897  facdiv  14238  hasheqf1oi  14302  relexpfld  15000  relexpuzrel  15003  reusq0  15416  climuni  15503  rlimno1  15605  sqrt2irr  16205  nn0rppwr  16519  prmdvdsexpr  16676  prmfac1  16679  dvdsprmpweqle  16846  ramlb  16979  ram0  16982  prmgaplem6  17016  prmlem1  17067  prmlem2  17079  pospo  18298  efgredlemc  19709  efgred  19712  ablsimpnosubgd  20070  sdrgacs  20767  prmirred  21462  psrvscafval  21936  fvmptnn04ifa  22824  fvmptnn04ifb  22825  fvmptnn04ifc  22826  fvmptnn04ifd  22827  chfacfscmulgsum  22834  chfacfpmmulgsum  22838  0top  22957  pnfnei  23194  mnfnei  23195  cmpfi  23382  1stccnp  23436  filconn  23857  ivthlem2  25428  ivthlem3  25429  ovolicc2lem3  25495  itg1addlem4  25675  itg2seq  25718  dvcnvlem  25952  lhop2  25992  bpos1  27265  lgsdir2lem2  27308  lgsqrlem2  27329  lgseisenlem2  27358  2sqnn  27421  pntlem3  27591  ostth3  27620  nosupbnd1lem5  27695  noinfbnd1lem5  27710  noetasuplem4  27719  noetainflem4  27723  elnnzs  28412  expsne0  28447  tgcgr4  28618  axlowdimlem15  29044  nbusgrvtxm1  29467  wlkv0  29738  1to2vfriswmgr  30369  n4cyclfrgr  30381  frgrnbnb  30383  frgrregord013  30485  snsssng  32604  ifeqeqx  32632  rprmdvdsprod  33614  fldext2chn  33893  f1resrcmplf1dlem  35250  erdszelem4  35397  erdszelem8  35401  antnestlaw3lem  35893  finminlem  36521  nn0prpwlem  36525  nn0prpw  36526  ordcmp  36650  axtcond  36681  mh-setindnd  36740  iooelexlt  37689  relowlssretop  37690  smprngopr  38384  disjlem14  39233  prtlem14  39331  atltcvr  39892  dihord6apre  41713  dihord6b  41717  jm2.23  43439  onexlimgt  43686  ordnexbtwnsuc  43710  onov0suclim  43717  relexpmulg  44152  rzalf  45463  or2expropbi  47479  nnmul2  47775  icceuelpart  47893  iccpartnel  47895  poprelb  47981  goldbachthlem2  48006  fmtnoprmfac1  48025  fmtnoprmfac2  48027  fmtno4prmfac  48032  fmtno4prmfac193  48033  2pwp1prm  48049  lighneallem4  48070  requad1  48095  requad2  48096  evenprm2  48187  odd2prm2  48191  stgoldbwt  48249  sbgoldbwt  48250  sbgoldbalt  48254  usgrexmpl12ngric  48511  pgnbgreunbgrlem2  48590  pgnbgreunbgrlem5  48596  ztprmneprm  48820  functermc  49980