Theorem pm2.21i 119

Description: A contradiction implies anything. Inference associated with pm2.21 123. Its associated inference is pm2.24ii 120. (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 114	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  120  notnotri  131  notnotriALT  132  pm2.21dd  195  pm3.2ni  881  falim  1559  rex0  4301  rmo0  4303  0ss  4341  rabsnifsb  4667  snsssn  4785  axnulALT  5239  dtrucor  5306  axc16b  5324  iresn0n0  6011  elfv2ex  6875  brfvopab  7415  el2mpocsbcl  8026  bropopvvv  8031  bropfvvvv  8033  tfrlem16  8323  omordi  8492  nnmordi  8558  omabs  8578  omsmolem  8584  0er  8673  pssnn  9094  fiint  9228  cantnfle  9581  r1sdom  9687  alephordi  9985  axdc3lem2  10362  canthp1  10566  elnnnn0b  12470  xltnegi  13157  xnn0xadd0  13188  xmulasslem2  13223  xrinf0  13280  elixx3g  13300  elfz2  13457  om2uzlti  13901  hashf1lem2  14407  hash3tpde  14444  relexpindlem  15014  sum0  15672  fsum2dlem  15721  prod0  15897  fprod2dlem  15934  nn0enne  16335  exprmfct  16663  prm23lt5  16774  4sqlem18  16922  vdwap0  16936  ram0  16982  prmlem1a  17066  prmlem2  17079  0catg  17643  dfgrp2e  18928  alexsub  24019  0met  24340  vitali  25589  plyeq0  26188  jensen  26970  ppiublem1  27184  ppiublem2  27185  lgsdir2lem3  27309  gausslemma2dlem0i  27346  2lgs  27389  2lgsoddprmlem3  27396  2sqnn  27421  2sqreultblem  27430  2sqreunnltblem  27433  rpvmasum  27508  ltssolem1  27658  nulslts  27786  nulsgts  27787  vtxdg0v  29562  0enwwlksnge1  29952  rusgr0edg  30064  frgrreggt1  30483  topnfbey  30559  n0lpligALT  30575  sgn3da  32927  sgnnbi  32931  sgnpbi  32932  isarchi  33263  constrmon  33909  sibf0  34499  signstfvneq0  34737  bnj98  35030  axnulALT2  35245  bisym1  36622  unqsym1  36628  bj-godellob  36883  poimirlem30  37982  axc5sp1  39380  areaquad  43659  cantnfresb  43767  succlg  43771  oacl2g  43773  omabs2  43775  omcl2  43776  fiiuncl  45511  iblempty  46408  vonhoire  47115  fveqvfvv  47485  ralndv1  47550  ndmaovcl  47648  mod2addne  47815  prmdvdsfmtnof1lem2  48045  31prm  48057  lighneallem3  48067  nprmdvdsfacm1lem2  48081  fpprbasnn  48202  sbgoldbaltlem1  48252  bgoldbtbndlem1  48278  stgr0  48433  upwlkbprop  48611