Theorem pm2.21d 122

Description: A contradiction implies anything. Deduction associated with pm2.21 124. (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 26	. 2 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))
3	2	con4d 116	1 ⊢ (𝜑 → (𝜓 → 𝜒))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  pm2.21ddALT  123  pm2.21  124  pm2.521g  175  prlem1  1070  sbc2or  3751  eq0rdvALT  4369  rzalALT  4454  reusv2lem2  5368  iunopeqop  5502  po2ne  5583  poirr2  6122  sofld  6184  f1resrcmplf1dlem  7274  dfwe2  7776  tfindsg  7860  findsg  7897  omopth2  8574  swoord2  8733  unxpdomlem3  9231  preleqg  9597  suc11reg  9601  wemapwe  9679  r111  9760  r1pwss  9769  cflim2  10268  axunndlem1  10607  axunnd  10608  axpowndlem3  10611  axpownd  10613  axregndlem1  10614  axregndlem2  10615  axinfndlem1  10617  axinfnd  10618  axacndlem1  10619  axacndlem2  10620  axacndlem3  10621  axacndlem4  10622  axacndlem5  10623  axacnd  10624  fpwwe2lem12  10654  gchpwdom  10682  winalim2  10708  ltapr  11057  prodgt0  12089  squeeze0  12145  nnsub  12307  nn0sub  12581  elnnz  12628  nn0lt10b  12686  indstr2  12979  uzsupss  12992  nn01to3  12993  xrltnsym  13190  xrlttr  13193  qbtwnxr  13254  xltnegi  13270  xmullem  13318  xlemul1a  13342  xrsupsslem  13361  xrinfmsslem  13362  xrub  13366  xrsup0  13377  xrinf0  13393  reltxrnmnf  13397  ixxdisj  13415  icodisj  13531  fzm1  13664  addmodlteq  14012  facdiv  14353  hasheqf1oi  14417  relexpfld  15124  relexpuzrel  15127  reusq0  15554  climuni  15641  rlimno1  15743  sqrt2irr  16341  nn0rppwr  16655  prmdvdsexpr  16812  prmfac1  16815  dvdsprmpweqle  16982  ramlb  17115  ram0  17118  prmgaplem6  17152  prmlem1  17203  prmlem2  17216  pospo  18435  efgredlemc  19876  efgred  19879  ablsimpnosubgd  20237  sdrgacs  20971  prmirred  21691  psrvscafval  22167  fvmptnn04ifa  23079  fvmptnn04ifb  23080  fvmptnn04ifc  23081  fvmptnn04ifd  23082  chfacfscmulgsum  23089  chfacfpmmulgsum  23093  0top  23212  pnfnei  23449  mnfnei  23450  cmpfi  23637  1stccnp  23692  filconn  24113  ivthlem2  25684  ivthlem3  25685  ovolicc2lem3  25751  itg1addlem4  25931  itg2seq  25974  dvcnvlem  26208  lhop2  26247  bpos1  27520  lgsdir2lem2  27563  lgsqrlem2  27584  lgseisenlem2  27613  2sqnn  27676  pntlem3  27846  ostth3  27875  nosupbnd1lem5  27949  noinfbnd1lem5  27964  noetasuplem4  27973  noetainflem4  27977  elnnzs  28667  expsne0  28702  tgcgr4  28874  axlowdimlem15  29414  nbusgrvtxm1  29840  wlkv0  30110  1to2vfriswmgr  30760  n4cyclfrgr  30772  frgrnbnb  30774  frgrregord013  30876  snsssng  32990  ifeqeqx  33018  rprmdvdsprod  33946  fldext2chn  34240  erdszelem4  35775  erdszelem8  35779  antnestlaw3lem  36271  finminlem  36939  nn0prpwlem  36943  nn0prpw  36944  ordcmp  37068  axtcond  37099  mh-setindnd  37158  iooelexlt  38118  relowlssretop  38119  smprngopr  38804  disjlem14  39651  prtlem14  39749  atltcvr  40310  dihord6apre  42131  dihord6b  42135  jm2.23  43839  onexlimgt  44086  ordnexbtwnsuc  44110  onov0suclim  44117  relexpmulg  44552  rzalf  45853  tmachlem-agreeprod  47767  or2expropbi  47924  nnmul2  48220  icceuelpart  48338  iccpartnel  48340  poprelb  48426  goldbachthlem2  48451  fmtnoprmfac1  48470  fmtnoprmfac2  48472  fmtno4prmfac  48477  fmtno4prmfac193  48478  2pwp1prm  48494  lighneallem4  48515  requad1  48540  requad2  48541  evenprm2  48632  odd2prm2  48636  stgoldbwt  48694  sbgoldbwt  48695  sbgoldbalt  48699  usgrexmpl12ngric  48956  pgnbgreunbgrlem2  49035  pgnbgreunbgrlem5  49041  smprngprmrng  49256  ztprmneprm  49279  functermc  50436