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  2falsedOLD  378  ecase2dOLD  1028  prlem1  1052  sbc2or  3726  eq0rdvALT  4340  rzalALT  4441  reusv2lem2  5323  po2ne  5520  poirr2  6034  sofld  6095  dfwe2  7633  tfindsg  7716  findsg  7755  omopth2  8424  swoord2  8539  unxpdomlem3  9038  preleqg  9382  suc11reg  9386  wemapwe  9464  r111  9542  r1pwss  9551  cflim2  10028  axunndlem1  10360  axunnd  10361  axpowndlem3  10364  axpownd  10366  axregndlem1  10367  axregndlem2  10368  axinfndlem1  10370  axinfnd  10371  axacndlem1  10372  axacndlem2  10373  axacndlem3  10374  axacndlem4  10375  axacndlem5  10376  axacnd  10377  fpwwe2lem12  10407  gchpwdom  10435  winalim2  10461  ltapr  10810  prodgt0  11831  squeeze0  11887  nnsub  12026  nn0sub  12292  elnnz  12338  nn0lt10b  12391  indstr2  12676  uzsupss  12689  nn01to3  12690  xrltnsym  12880  xrlttr  12883  qbtwnxr  12943  xltnegi  12959  xmullem  13007  xlemul1a  13031  xrsupsslem  13050  xrinfmsslem  13051  xrub  13055  xrsup0  13066  xrinf0  13081  reltxrnmnf  13085  ixxdisj  13103  icodisj  13217  fzm1  13345  addmodlteq  13675  facdiv  14010  hasheqf1oi  14075  relexpfld  14769  relexpuzrel  14772  reusq0  15183  climuni  15270  rlimno1  15374  sqrt2irr  15967  prmdvdsexpr  16431  prmfac1  16435  dvdsprmpweqle  16596  ramlb  16729  ram0  16732  prmgaplem6  16766  prmlem1  16818  prmlem2  16830  pospo  18072  efgredlemc  19360  efgred  19363  ablsimpnosubgd  19716  sdrgacs  20078  prmirred  20705  psrvscafval  21168  fvmptnn04ifa  22008  fvmptnn04ifb  22009  fvmptnn04ifc  22010  fvmptnn04ifd  22011  chfacfscmulgsum  22018  chfacfpmmulgsum  22022  0top  22142  pnfnei  22380  mnfnei  22381  cmpfi  22568  1stccnp  22622  filconn  23043  ivthlem2  24625  ivthlem3  24626  ovolicc2lem3  24692  itg1addlem4  24872  itg1addlem4OLD  24873  itg2seq  24916  dvcnvlem  25149  lhop2  25188  bpos1  26440  lgsdir2lem2  26483  lgsqrlem2  26504  lgseisenlem2  26533  2sqnn  26596  pntlem3  26766  ostth3  26795  tgcgr4  26901  axlowdimlem15  27333  nbusgrvtxm1  27755  wlkv0  28027  1to2vfriswmgr  28652  n4cyclfrgr  28664  frgrnbnb  28666  frgrregord013  28768  snsssng  30869  ifeqeqx  30894  f1resrcmplf1dlem  33067  erdszelem4  33165  erdszelem8  33169  nosupbnd1lem5  33924  noinfbnd1lem5  33939  noetasuplem4  33948  noetainflem4  33952  finminlem  34516  nn0prpwlem  34520  nn0prpw  34521  ordcmp  34645  iooelexlt  35542  relowlssretop  35543  smprngopr  36219  prtlem14  36895  atltcvr  37456  dihord6apre  39277  dihord6b  39281  nn0rppwr  40340  jm2.23  40825  rp-fakeimass  41126  relexpmulg  41325  rzalf  42567  or2expropbi  44539  icceuelpart  44899  iccpartnel  44901  poprelb  44987  goldbachthlem2  45009  fmtnoprmfac1  45028  fmtnoprmfac2  45030  fmtno4prmfac  45035  fmtno4prmfac193  45036  2pwp1prm  45052  lighneallem4  45073  requad1  45085  requad2  45086  evenprm2  45177  odd2prm2  45181  stgoldbwt  45239  sbgoldbwt  45240  sbgoldbalt  45244  ztprmneprm  45694