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  4314  rmo0  4316  0ss  4354  rabsnifsb  4681  snsssn  4799  axnulALT  5251  dtrucor  5318  axc16b  5336  iresn0n0  6021  elfv2ex  6885  brfvopab  7425  el2mpocsbcl  8037  bropopvvv  8042  bropfvvvv  8044  tfrlem16  8334  omordi  8503  nnmordi  8569  omabs  8589  omsmolem  8595  0er  8684  pssnn  9105  fiint  9239  cantnfle  9592  r1sdom  9698  alephordi  9996  axdc3lem2  10373  canthp1  10577  elnnnn0b  12457  xltnegi  13143  xnn0xadd0  13174  xmulasslem2  13209  xrinf0  13266  elixx3g  13286  elfz2  13442  om2uzlti  13885  hashf1lem2  14391  hash3tpde  14428  relexpindlem  14998  sum0  15656  fsum2dlem  15705  prod0  15878  fprod2dlem  15915  nn0enne  16316  exprmfct  16643  prm23lt5  16754  4sqlem18  16902  vdwap0  16916  ram0  16962  prmlem1a  17046  prmlem2  17059  0catg  17623  dfgrp2e  18905  alexsub  24001  0met  24322  vitali  25582  plyeq0  26184  jensen  26967  ppiublem1  27181  ppiublem2  27182  lgsdir2lem3  27306  gausslemma2dlem0i  27343  2lgs  27386  2lgsoddprmlem3  27393  2sqnn  27418  2sqreultblem  27427  2sqreunnltblem  27430  rpvmasum  27505  ltssolem1  27655  nulslts  27783  nulsgts  27784  vtxdg0v  29559  0enwwlksnge1  29949  rusgr0edg  30061  frgrreggt1  30480  topnfbey  30556  n0lpligALT  30571  sgn3da  32925  sgnnbi  32929  sgnpbi  32930  isarchi  33275  constrmon  33921  sibf0  34511  signstfvneq0  34749  bnj98  35042  bisym1  36632  unqsym1  36638  bj-godellob  36826  poimirlem30  37890  axc5sp1  39288  areaquad  43562  cantnfresb  43670  succlg  43674  oacl2g  43676  omabs2  43678  omcl2  43679  fiiuncl  45414  iblempty  46312  vonhoire  47019  fveqvfvv  47389  ralndv1  47454  ndmaovcl  47552  mod2addne  47713  prmdvdsfmtnof1lem2  47934  31prm  47946  lighneallem3  47956  fpprbasnn  48078  sbgoldbaltlem1  48128  bgoldbtbndlem1  48154  stgr0  48309  upwlkbprop  48487