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  377  ecase2dOLD  1027  prlem1  1051  sbc2or  3720  eq0rdvALT  4336  rzalALT  4437  reusv2lem2  5317  po2ne  5510  poirr2  6018  sofld  6079  dfwe2  7602  tfindsg  7682  findsg  7720  omopth2  8377  swoord2  8488  unxpdomlem3  8958  preleqg  9303  suc11reg  9307  wemapwe  9385  r111  9464  r1pwss  9473  cflim2  9950  axunndlem1  10282  axunnd  10283  axpowndlem3  10286  axpownd  10288  axregndlem1  10289  axregndlem2  10290  axinfndlem1  10292  axinfnd  10293  axacndlem1  10294  axacndlem2  10295  axacndlem3  10296  axacndlem4  10297  axacndlem5  10298  axacnd  10299  fpwwe2lem12  10329  gchpwdom  10357  winalim2  10383  ltapr  10732  prodgt0  11752  squeeze0  11808  nnsub  11947  nn0sub  12213  elnnz  12259  nn0lt10b  12312  indstr2  12596  uzsupss  12609  nn01to3  12610  xrltnsym  12800  xrlttr  12803  qbtwnxr  12863  xltnegi  12879  xmullem  12927  xlemul1a  12951  xrsupsslem  12970  xrinfmsslem  12971  xrub  12975  xrsup0  12986  xrinf0  13001  reltxrnmnf  13005  ixxdisj  13023  icodisj  13137  fzm1  13265  addmodlteq  13594  facdiv  13929  hasheqf1oi  13994  relexpfld  14688  relexpuzrel  14691  reusq0  15102  climuni  15189  rlimno1  15293  sqrt2irr  15886  prmdvdsexpr  16350  prmfac1  16354  dvdsprmpweqle  16515  ramlb  16648  ram0  16651  prmgaplem6  16685  prmlem1  16737  prmlem2  16749  pospo  17978  efgredlemc  19266  efgred  19269  ablsimpnosubgd  19622  sdrgacs  19984  prmirred  20608  psrvscafval  21069  fvmptnn04ifa  21907  fvmptnn04ifb  21908  fvmptnn04ifc  21909  fvmptnn04ifd  21910  chfacfscmulgsum  21917  chfacfpmmulgsum  21921  0top  22041  pnfnei  22279  mnfnei  22280  cmpfi  22467  1stccnp  22521  filconn  22942  ivthlem2  24521  ivthlem3  24522  ovolicc2lem3  24588  itg1addlem4  24768  itg1addlem4OLD  24769  itg2seq  24812  dvcnvlem  25045  lhop2  25084  bpos1  26336  lgsdir2lem2  26379  lgsqrlem2  26400  lgseisenlem2  26429  2sqnn  26492  pntlem3  26662  ostth3  26691  tgcgr4  26796  axlowdimlem15  27227  nbusgrvtxm1  27649  wlkv0  27920  1to2vfriswmgr  28544  n4cyclfrgr  28556  frgrnbnb  28558  frgrregord013  28660  snsssng  30761  ifeqeqx  30786  f1resrcmplf1dlem  32958  erdszelem4  33056  erdszelem8  33060  nosupbnd1lem5  33842  noinfbnd1lem5  33857  noetasuplem4  33866  noetainflem4  33870  finminlem  34434  nn0prpwlem  34438  nn0prpw  34439  ordcmp  34563  iooelexlt  35460  relowlssretop  35461  smprngopr  36137  prtlem14  36815  atltcvr  37376  dihord6apre  39197  dihord6b  39201  nn0rppwr  40254  jm2.23  40734  rp-fakeimass  41017  relexpmulg  41207  rzalf  42449  or2expropbi  44415  icceuelpart  44776  iccpartnel  44778  poprelb  44864  goldbachthlem2  44886  fmtnoprmfac1  44905  fmtnoprmfac2  44907  fmtno4prmfac  44912  fmtno4prmfac193  44913  2pwp1prm  44929  lighneallem4  44950  requad1  44962  requad2  44963  evenprm2  45054  odd2prm2  45058  stgoldbwt  45116  sbgoldbwt  45117  sbgoldbalt  45121  ztprmneprm  45571