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  27782  axlowdimlem15  28214  nbusgrvtxm1  28636  wlkv0  28908  1to2vfriswmgr  29532  n4cyclfrgr  29544  frgrnbnb  29546  frgrregord013  29648  snsssng  31752  ifeqeqx  31774  f1resrcmplf1dlem  34089  erdszelem4  34185  erdszelem8  34189  finminlem  35203  nn0prpwlem  35207  nn0prpw  35208  ordcmp  35332  iooelexlt  36243  relowlssretop  36244  smprngopr  36920  disjlem14  37668  prtlem14  37744  atltcvr  38306  dihord6apre  40127  dihord6b  40131  nn0rppwr  41224  jm2.23  41735  onexlimgt  41992  ordnexbtwnsuc  42017  onov0suclim  42024  relexpmulg  42461  rzalf  43701  or2expropbi  45744  icceuelpart  46104  iccpartnel  46106  poprelb  46192  goldbachthlem2  46214  fmtnoprmfac1  46233  fmtnoprmfac2  46235  fmtno4prmfac  46240  fmtno4prmfac193  46241  2pwp1prm  46257  lighneallem4  46278  requad1  46290  requad2  46291  evenprm2  46382  odd2prm2  46386  stgoldbwt  46444  sbgoldbwt  46445  sbgoldbalt  46449  ztprmneprm  47023