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  1030  prlem1  1054  sbc2or  3787  eq0rdvALT  4406  rzalALT  4510  reusv2lem2  5398  po2ne  5605  poirr2  6126  sofld  6187  dfwe2  7761  tfindsg  7850  findsg  7890  omopth2  8584  swoord2  8735  unxpdomlem3  9252  preleqg  9610  suc11reg  9614  wemapwe  9692  r111  9770  r1pwss  9779  cflim2  10258  axunndlem1  10590  axunnd  10591  axpowndlem3  10594  axpownd  10596  axregndlem1  10597  axregndlem2  10598  axinfndlem1  10600  axinfnd  10601  axacndlem1  10602  axacndlem2  10603  axacndlem3  10604  axacndlem4  10605  axacndlem5  10606  axacnd  10607  fpwwe2lem12  10637  gchpwdom  10665  winalim2  10691  ltapr  11040  prodgt0  12061  squeeze0  12117  nnsub  12256  nn0sub  12522  elnnz  12568  nn0lt10b  12624  indstr2  12911  uzsupss  12924  nn01to3  12925  xrltnsym  13116  xrlttr  13119  qbtwnxr  13179  xltnegi  13195  xmullem  13243  xlemul1a  13267  xrsupsslem  13286  xrinfmsslem  13287  xrub  13291  xrsup0  13302  xrinf0  13317  reltxrnmnf  13321  ixxdisj  13339  icodisj  13453  fzm1  13581  addmodlteq  13911  facdiv  14247  hasheqf1oi  14311  relexpfld  14996  relexpuzrel  14999  reusq0  15409  climuni  15496  rlimno1  15600  sqrt2irr  16192  prmdvdsexpr  16654  prmfac1  16658  dvdsprmpweqle  16819  ramlb  16952  ram0  16955  prmgaplem6  16989  prmlem1  17041  prmlem2  17053  pospo  18298  efgredlemc  19613  efgred  19616  ablsimpnosubgd  19974  sdrgacs  20417  prmirred  21044  psrvscafval  21509  fvmptnn04ifa  22352  fvmptnn04ifb  22353  fvmptnn04ifc  22354  fvmptnn04ifd  22355  chfacfscmulgsum  22362  chfacfpmmulgsum  22366  0top  22486  pnfnei  22724  mnfnei  22725  cmpfi  22912  1stccnp  22966  filconn  23387  ivthlem2  24969  ivthlem3  24970  ovolicc2lem3  25036  itg1addlem4  25216  itg1addlem4OLD  25217  itg2seq  25260  dvcnvlem  25493  lhop2  25532  bpos1  26786  lgsdir2lem2  26829  lgsqrlem2  26850  lgseisenlem2  26879  2sqnn  26942  pntlem3  27112  ostth3  27141  nosupbnd1lem5  27215  noinfbnd1lem5  27230  noetasuplem4  27239  noetainflem4  27243  tgcgr4  27813  axlowdimlem15  28245  nbusgrvtxm1  28667  wlkv0  28939  1to2vfriswmgr  29563  n4cyclfrgr  29575  frgrnbnb  29577  frgrregord013  29679  snsssng  31783  ifeqeqx  31805  f1resrcmplf1dlem  34120  erdszelem4  34216  erdszelem8  34220  finminlem  35251  nn0prpwlem  35255  nn0prpw  35256  ordcmp  35380  iooelexlt  36291  relowlssretop  36292  smprngopr  36968  disjlem14  37716  prtlem14  37792  atltcvr  38354  dihord6apre  40175  dihord6b  40179  nn0rppwr  41272  jm2.23  41783  onexlimgt  42040  ordnexbtwnsuc  42065  onov0suclim  42072  relexpmulg  42509  rzalf  43749  or2expropbi  45792  icceuelpart  46152  iccpartnel  46154  poprelb  46240  goldbachthlem2  46262  fmtnoprmfac1  46281  fmtnoprmfac2  46283  fmtno4prmfac  46288  fmtno4prmfac193  46289  2pwp1prm  46305  lighneallem4  46326  requad1  46338  requad2  46339  evenprm2  46430  odd2prm2  46434  stgoldbwt  46492  sbgoldbwt  46493  sbgoldbalt  46497  ztprmneprm  47071