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  prlem1  1060  sbc2or  3739  eq0rdvALT  4343  rzalALT  4430  reusv2lem2  5335  iunopeqop  5469  po2ne  5549  poirr2  6081  sofld  6145  dfwe2  7724  tfindsg  7808  findsg  7844  omopth2  8516  swoord2  8674  unxpdomlem3  9165  preleqg  9534  suc11reg  9538  wemapwe  9616  r111  9697  r1pwss  9706  cflim2  10183  axunndlem1  10516  axunnd  10517  axpowndlem3  10520  axpownd  10522  axregndlem1  10523  axregndlem2  10524  axinfndlem1  10526  axinfnd  10527  axacndlem1  10528  axacndlem2  10529  axacndlem3  10530  axacndlem4  10531  axacndlem5  10532  axacnd  10533  fpwwe2lem12  10563  gchpwdom  10591  winalim2  10617  ltapr  10966  prodgt0  12000  squeeze0  12057  nnsub  12219  nn0sub  12485  elnnz  12532  nn0lt10b  12589  indstr2  12875  uzsupss  12888  nn01to3  12889  xrltnsym  13086  xrlttr  13089  qbtwnxr  13150  xltnegi  13166  xmullem  13214  xlemul1a  13238  xrsupsslem  13257  xrinfmsslem  13258  xrub  13262  xrsup0  13273  xrinf0  13289  reltxrnmnf  13293  ixxdisj  13311  icodisj  13427  fzm1  13559  addmodlteq  13906  facdiv  14247  hasheqf1oi  14311  relexpfld  15009  relexpuzrel  15012  reusq0  15425  climuni  15512  rlimno1  15614  sqrt2irr  16214  nn0rppwr  16528  prmdvdsexpr  16685  prmfac1  16688  dvdsprmpweqle  16855  ramlb  16988  ram0  16991  prmgaplem6  17025  prmlem1  17076  prmlem2  17088  pospo  18307  efgredlemc  19718  efgred  19721  ablsimpnosubgd  20079  sdrgacs  20780  prmirred  21456  psrvscafval  21930  fvmptnn04ifa  22840  fvmptnn04ifb  22841  fvmptnn04ifc  22842  fvmptnn04ifd  22843  chfacfscmulgsum  22850  chfacfpmmulgsum  22854  0top  22973  pnfnei  23210  mnfnei  23211  cmpfi  23398  1stccnp  23452  filconn  23873  ivthlem2  25444  ivthlem3  25445  ovolicc2lem3  25511  itg1addlem4  25691  itg2seq  25734  dvcnvlem  25968  lhop2  26007  bpos1  27271  lgsdir2lem2  27314  lgsqrlem2  27335  lgseisenlem2  27364  2sqnn  27427  pntlem3  27597  ostth3  27626  nosupbnd1lem5  27701  noinfbnd1lem5  27716  noetasuplem4  27725  noetainflem4  27729  elnnzs  28418  expsne0  28453  tgcgr4  28624  axlowdimlem15  29050  nbusgrvtxm1  29473  wlkv0  29743  1to2vfriswmgr  30374  n4cyclfrgr  30386  frgrnbnb  30388  frgrregord013  30490  snsssng  32609  ifeqeqx  32637  rprmdvdsprod  33624  fldext2chn  33919  f1resrcmplf1dlem  35276  erdszelem4  35423  erdszelem8  35427  antnestlaw3lem  35919  finminlem  36547  nn0prpwlem  36551  nn0prpw  36552  ordcmp  36676  axtcond  36707  mh-setindnd  36766  iooelexlt  37725  relowlssretop  37726  smprngopr  38420  disjlem14  39269  prtlem14  39367  atltcvr  39928  dihord6apre  41749  dihord6b  41753  jm2.23  43442  onexlimgt  43689  ordnexbtwnsuc  43713  onov0suclim  43720  relexpmulg  44155  rzalf  45466  or2expropbi  47498  nnmul2  47794  icceuelpart  47912  iccpartnel  47914  poprelb  48000  goldbachthlem2  48025  fmtnoprmfac1  48044  fmtnoprmfac2  48046  fmtno4prmfac  48051  fmtno4prmfac193  48052  2pwp1prm  48068  lighneallem4  48089  requad1  48114  requad2  48115  evenprm2  48206  odd2prm2  48210  stgoldbwt  48268  sbgoldbwt  48269  sbgoldbalt  48273  usgrexmpl12ngric  48530  pgnbgreunbgrlem2  48609  pgnbgreunbgrlem5  48615  ztprmneprm  48839  functermc  49999