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 ⊢ (𝜑 → (𝜓 → 𝜒))

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  123  pm2.21  124  pm2.521g  175  prlem1  1068  sbc2or  3752  eq0rdvALT  4372  rzalALT  4455  reusv2lem2  5370  iunopeqop  5504  po2ne  5585  poirr2  6124  sofld  6185  dfwe2  7772  tfindsg  7856  findsg  7893  omopth2  8568  swoord2  8727  unxpdomlem3  9217  preleqg  9583  suc11reg  9587  wemapwe  9665  r111  9746  r1pwss  9755  cflim2  10246  axunndlem1  10579  axunnd  10580  axpowndlem3  10583  axpownd  10585  axregndlem1  10586  axregndlem2  10587  axinfndlem1  10589  axinfnd  10590  axacndlem1  10591  axacndlem2  10592  axacndlem3  10593  axacndlem4  10594  axacndlem5  10595  axacnd  10596  fpwwe2lem12  10626  gchpwdom  10654  winalim2  10680  ltapr  11029  prodgt0  12061  squeeze0  12117  nnsub  12279  nn0sub  12553  elnnz  12600  nn0lt10b  12657  indstr2  12950  uzsupss  12963  nn01to3  12964  xrltnsym  13161  xrlttr  13164  qbtwnxr  13225  xltnegi  13241  xmullem  13289  xlemul1a  13313  xrsupsslem  13332  xrinfmsslem  13333  xrub  13337  xrsup0  13348  xrinf0  13364  reltxrnmnf  13368  ixxdisj  13386  icodisj  13502  fzm1  13635  addmodlteq  13982  facdiv  14323  hasheqf1oi  14387  relexpfld  15086  relexpuzrel  15089  reusq0  15516  climuni  15603  rlimno1  15705  sqrt2irr  16304  nn0rppwr  16618  prmdvdsexpr  16775  prmfac1  16778  dvdsprmpweqle  16945  ramlb  17078  ram0  17081  prmgaplem6  17115  prmlem1  17166  prmlem2  17179  pospo  18398  efgredlemc  19814  efgred  19817  ablsimpnosubgd  20175  sdrgacs  20883  prmirred  21603  psrvscafval  22077  fvmptnn04ifa  22986  fvmptnn04ifb  22987  fvmptnn04ifc  22988  fvmptnn04ifd  22989  chfacfscmulgsum  22996  chfacfpmmulgsum  23000  0top  23119  pnfnei  23356  mnfnei  23357  cmpfi  23544  1stccnp  23598  filconn  24019  ivthlem2  25590  ivthlem3  25591  ovolicc2lem3  25657  itg1addlem4  25837  itg2seq  25880  dvcnvlem  26114  lhop2  26153  bpos1  27423  lgsdir2lem2  27466  lgsqrlem2  27487  lgseisenlem2  27516  2sqnn  27579  pntlem3  27749  ostth3  27778  nosupbnd1lem5  27852  noinfbnd1lem5  27867  noetasuplem4  27876  noetainflem4  27880  elnnzs  28570  expsne0  28605  tgcgr4  28776  axlowdimlem15  29272  nbusgrvtxm1  29695  wlkv0  29965  1to2vfriswmgr  30596  n4cyclfrgr  30608  frgrnbnb  30610  frgrregord013  30712  snsssng  32826  ifeqeqx  32854  rprmdvdsprod  33790  fldext2chn  34084  f1resrcmplf1dlem  35440  erdszelem4  35652  erdszelem8  35656  antnestlaw3lem  36148  finminlem  36795  nn0prpwlem  36799  nn0prpw  36800  ordcmp  36924  axtcond  36955  mh-setindnd  37014  iooelexlt  37974  relowlssretop  37975  smprngopr  38669  disjlem14  39518  prtlem14  39616  atltcvr  40177  dihord6apre  41998  dihord6b  42002  jm2.23  43693  onexlimgt  43940  ordnexbtwnsuc  43964  onov0suclim  43971  relexpmulg  44406  rzalf  45707  or2expropbi  47738  nnmul2  48034  icceuelpart  48152  iccpartnel  48154  poprelb  48240  goldbachthlem2  48265  fmtnoprmfac1  48284  fmtnoprmfac2  48286  fmtno4prmfac  48291  fmtno4prmfac193  48292  2pwp1prm  48308  lighneallem4  48329  requad1  48354  requad2  48355  evenprm2  48446  odd2prm2  48450  stgoldbwt  48508  sbgoldbwt  48509  sbgoldbalt  48513  usgrexmpl12ngric  48770  pgnbgreunbgrlem2  48849  pgnbgreunbgrlem5  48855  smprngprmrng  49071  ztprmneprm  49094  functermc  50253