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  1586  rex0  4307  rmo0  4309  0ss  4349  rabsnifsb  4679  snsssn  4795  axnulALT  5257  dtrucor  5332  axc16b  5350  iresn0n0  6045  elfv2ex  6929  brfvopab  7478  el2mpocsbcl  8097  bropopvvv  8102  bropfvvvv  8104  tfrlem16  8405  omordi  8578  nnmordi  8644  omabs  8664  omsmolem  8670  0er  8760  pssnn  9188  fiint  9322  cantnfle  9676  r1sdom  9785  alephordi  10157  axdc3lem2  10533  canthp1  10743  elnnnn0b  12654  xltnegi  13350  xnn0xadd0  13381  xmulasslem2  13416  xrinf0  13473  elixx3g  13493  elfz2  13650  om2uzlti  14097  hashf1lem2  14605  hash3tpde  14642  relexpindlem  15222  sgn3da  15260  sgnnbi  15263  sgnpbi  15264  sum0  15893  fsum2dlem  15942  prod0  16116  fprod2dlem  16153  nn0enne  16553  exprmfct  16886  prm23lt5  16998  4sqlem18  17146  vdwap0  17160  ram0  17206  prmlem1a  17290  prmlem2  17304  0catg  17868  dfgrp2e  19180  alexsub  24370  0met  24691  vitali  25940  plyeq0  26536  jensen  27322  ppiublem1  27535  ppiublem2  27536  lgsdir2lem3  27660  gausslemma2dlem0i  27697  2lgs  27740  2lgsoddprmlem3  27747  2sqnn  27772  2sqreultblem  27781  2sqreunnltblem  27784  rpvmasum  27859  ltssolem1  28038  nulslts  28167  nulsgts  28168  vtxdg0v  30060  0enwwlksnge1  30459  rusgr0edg  30571  frgrreggt1  31000  topnfbey  31076  n0lpligALT  31092  isarchi  33790  constrmon  34423  sibf0  35013  signstfvneq0  35248  bnj98  35544  axnulALT2  35761  bisym1  37300  unqsym1  37306  bj-godellob  37568  poimirlem30  38662  axc5sp1  40074  areaquad  44312  cantnfresb  44420  succlg  44424  oacl2g  44426  omabs2  44428  omcl2  44429  fiiuncl  46176  iblempty  47069  vonhoire  47776  fveqvfvv  48204  ralndv1  48269  ndmaovcl  48367  mod2addne  48534  prmdvdsfmtnof1lem2  48764  31prm  48776  lighneallem3  48786  nprmdvdsfacm1lem2  48800  fpprbasnn  48921  sbgoldbaltlem1  48971  bgoldbtbndlem1  48997  stgr0  49152  upwlkbprop  49330  prmringnzring  49528