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  196  pm3.2ni  886  falim  1564  rex0  4295  rmo0  4297  0ss  4335  rabsnifsb  4661  snsssn  4779  axnulALT  5233  dtrucor  5307  axc16b  5325  iresn0n0  6013  elfv2ex  6877  brfvopab  7420  el2mpocsbcl  8031  bropopvvv  8036  bropfvvvv  8038  tfrlem16  8329  omordi  8498  nnmordi  8564  omabs  8584  omsmolem  8590  0er  8679  pssnn  9100  fiint  9234  cantnfle  9590  r1sdom  9696  alephordi  9994  axdc3lem2  10371  canthp1  10575  elnnnn0b  12479  xltnegi  13166  xnn0xadd0  13197  xmulasslem2  13232  xrinf0  13289  elixx3g  13309  elfz2  13466  om2uzlti  13910  hashf1lem2  14416  hash3tpde  14453  relexpindlem  15023  sum0  15681  fsum2dlem  15730  prod0  15906  fprod2dlem  15943  nn0enne  16344  exprmfct  16672  prm23lt5  16783  4sqlem18  16931  vdwap0  16945  ram0  16991  prmlem1a  17075  prmlem2  17088  0catg  17652  dfgrp2e  18937  alexsub  24035  0met  24356  vitali  25605  plyeq0  26201  jensen  26977  ppiublem1  27190  ppiublem2  27191  lgsdir2lem3  27315  gausslemma2dlem0i  27352  2lgs  27395  2lgsoddprmlem3  27402  2sqnn  27427  2sqreultblem  27436  2sqreunnltblem  27439  rpvmasum  27514  ltssolem1  27664  nulslts  27792  nulsgts  27793  vtxdg0v  29567  0enwwlksnge1  29957  rusgr0edg  30069  frgrreggt1  30488  topnfbey  30564  n0lpligALT  30580  sgn3da  32933  sgnnbi  32937  sgnpbi  32938  isarchi  33270  constrmon  33935  sibf0  34525  signstfvneq0  34763  bnj98  35056  axnulALT2  35271  bisym1  36654  unqsym1  36660  bj-godellob  36923  poimirlem30  38024  axc5sp1  39422  areaquad  43668  cantnfresb  43776  succlg  43780  oacl2g  43782  omabs2  43784  omcl2  43785  fiiuncl  45520  iblempty  46415  vonhoire  47122  fveqvfvv  47510  ralndv1  47575  ndmaovcl  47673  mod2addne  47840  prmdvdsfmtnof1lem2  48070  31prm  48082  lighneallem3  48092  nprmdvdsfacm1lem2  48106  fpprbasnn  48227  sbgoldbaltlem1  48277  bgoldbtbndlem1  48303  stgr0  48458  upwlkbprop  48636