Theorem pm2.21i 120

Description: A contradiction implies anything. Inference associated with pm2.21 124. Its associated inference is pm2.24ii 121. (Contributed by NM, 16-Sep-1993.)

Hypothesis

Ref	Expression
pm2.21i.1	⊢ ¬ 𝜑

Assertion

Ref	Expression
pm2.21i	⊢ (𝜑 → 𝜓)

Proof of Theorem pm2.21i

Step	Hyp	Ref	Expression
1		pm2.21i.1	. . 3 ⊢ ¬ 𝜑
2	1	a1i 11	. 2 ⊢ (¬ 𝜓 → ¬ 𝜑)
3	2	con4i 115	1 ⊢ (𝜑 → 𝜓)

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-3 8

This theorem is referenced by:  pm2.24ii  121  notnotri  132  notnotriALT  133  pm2.21dd  198  pm3.2ni  893  falim  1587  rex0  4316  rmo0  4318  0ss  4358  rabsnifsb  4689  snsssn  4807  axnulALT  5268  dtrucor  5344  axc16b  5362  iresn0n0  6058  elfv2ex  6926  brfvopab  7469  el2mpocsbcl  8081  bropopvvv  8086  bropfvvvv  8088  tfrlem16  8381  omordi  8552  nnmordi  8618  omabs  8638  omsmolem  8644  0er  8734  pssnn  9154  fiint  9287  cantnfle  9641  r1sdom  9747  alephordi  10059  axdc3lem2  10436  canthp1  10640  elnnnn0b  12549  xltnegi  13243  xnn0xadd0  13274  xmulasslem2  13309  xrinf0  13366  elixx3g  13386  elfz2  13543  om2uzlti  13988  hashf1lem2  14495  hash3tpde  14532  relexpindlem  15102  sgn3da  15140  sgnnbi  15143  sgnpbi  15144  sum0  15774  fsum2dlem  15823  prod0  15999  fprod2dlem  16036  nn0enne  16436  exprmfct  16764  prm23lt5  16875  4sqlem18  17023  vdwap0  17037  ram0  17083  prmlem1a  17167  prmlem2  17181  0catg  17745  dfgrp2e  19031  alexsub  24183  0met  24504  vitali  25753  plyeq0  26349  jensen  27134  ppiublem1  27347  ppiublem2  27348  lgsdir2lem3  27472  gausslemma2dlem0i  27509  2lgs  27552  2lgsoddprmlem3  27559  2sqnn  27584  2sqreultblem  27593  2sqreunnltblem  27596  rpvmasum  27671  ltssolem1  27820  nulslts  27949  nulsgts  27950  vtxdg0v  29804  0enwwlksnge1  30194  rusgr0edg  30306  frgrreggt1  30725  topnfbey  30801  n0lpligALT  30817  isarchi  33483  constrmon  34115  sibf0  34705  signstfvneq0  34940  bnj98  35236  axnulALT2  35452  bisym1  36911  unqsym1  36917  bj-godellob  37179  poimirlem30  38282  axc5sp1  39678  areaquad  43926  cantnfresb  44034  succlg  44038  oacl2g  44040  omabs2  44042  omcl2  44043  fiiuncl  45768  iblempty  46662  vonhoire  47369  fveqvfvv  47760  ralndv1  47825  ndmaovcl  47923  mod2addne  48090  prmdvdsfmtnof1lem2  48320  31prm  48332  lighneallem3  48342  nprmdvdsfacm1lem2  48356  fpprbasnn  48477  sbgoldbaltlem1  48527  bgoldbtbndlem1  48553  stgr0  48708  upwlkbprop  48886  prmringnzring  49085