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 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-3 8

This theorem is used by:  pm2.24ii  121  notnotri  132  notnotriALT  133  pm2.21dd  198  pm3.2ni  894  falim  1587  rex0  4311  rmo0  4313  0ss  4353  rabsnifsb  4683  snsssn  4799  axnulALT  5262  dtrucor  5338  axc16b  5356  iresn0n0  6059  elfv2ex  6954  brfvopab  7503  el2mpocsbcl  8124  bropopvvv  8129  bropfvvvv  8131  tfrlem16  8432  omordi  8605  nnmordi  8671  omabs  8691  omsmolem  8697  0er  8787  pssnn  9215  fiint  9349  cantnfle  9702  r1sdom  9811  alephordi  10183  axdc3lem2  10559  canthp1  10769  elnnnn0b  12680  xltnegi  13376  xnn0xadd0  13407  xmulasslem2  13442  xrinf0  13499  elixx3g  13519  elfz2  13676  om2uzlti  14123  hashf1lem2  14631  hash3tpde  14668  relexpindlem  15248  sgn3da  15286  sgnnbi  15289  sgnpbi  15290  sum0  15919  fsum2dlem  15968  prod0  16142  fprod2dlem  16179  nn0enne  16579  exprmfct  16912  prm23lt5  17024  4sqlem18  17172  vdwap0  17186  ram0  17232  prmlem1a  17316  prmlem2  17330  0catg  17894  dfgrp2e  19206  alexsub  24397  0met  24718  vitali  25967  plyeq0  26563  jensen  27349  ppiublem1  27562  ppiublem2  27563  lgsdir2lem3  27687  gausslemma2dlem0i  27724  2lgs  27767  2lgsoddprmlem3  27774  2sqnn  27799  2sqreultblem  27808  2sqreunnltblem  27811  rpvmasum  27886  ltssolem1  28065  nulslts  28194  nulsgts  28195  vtxdg0v  30087  0enwwlksnge1  30486  rusgr0edg  30598  frgrreggt1  31027  topnfbey  31103  n0lpligALT  31119  isarchi  33819  constrmon  34459  sibf0  35049  signstfvneq0  35284  bnj98  35580  axnulALT2  35797  bisym1  37398  unqsym1  37404  bj-godellob  37666  poimirlem30  38773  axc5sp1  40183  areaquad  44421  cantnfresb  44529  succlg  44533  oacl2g  44535  omabs2  44537  omcl2  44538  fiiuncl  46298  iblempty  47190  vonhoire  47897  fveqvfvv  48325  ralndv1  48391  ndmaovcl  48488  mod2addne  48655  prmdvdsfmtnof1lem2  48885  31prm  48897  lighneallem3  48907  nprmdvdsfacm1lem2  48921  fpprbasnn  49042  sbgoldbaltlem1  49092  bgoldbtbndlem1  49118  stgr0  49273  upwlkbprop  49451  prmringnzring  49649