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  4318  rmo0  4320  0ss  4360  rabsnifsb  4693  snsssn  4811  axnulALT  5272  dtrucor  5347  axc16b  5365  iresn0n0  6061  elfv2ex  6931  brfvopab  7480  el2mpocsbcl  8089  bropopvvv  8094  bropfvvvv  8096  tfrlem16  8389  omordi  8560  nnmordi  8626  omabs  8646  omsmolem  8652  0er  8742  pssnn  9163  fiint  9296  cantnfle  9650  r1sdom  9756  alephordi  10077  axdc3lem2  10453  canthp1  10657  elnnnn0b  12566  xltnegi  13260  xnn0xadd0  13291  xmulasslem2  13326  xrinf0  13383  elixx3g  13403  elfz2  13560  om2uzlti  14006  hashf1lem2  14513  hash3tpde  14550  relexpindlem  15126  sgn3da  15164  sgnnbi  15167  sgnpbi  15168  sum0  15798  fsum2dlem  15847  prod0  16023  fprod2dlem  16060  nn0enne  16460  exprmfct  16788  prm23lt5  16899  4sqlem18  17047  vdwap0  17061  ram0  17107  prmlem1a  17191  prmlem2  17205  0catg  17769  dfgrp2e  19061  alexsub  24239  0met  24560  vitali  25809  plyeq0  26405  jensen  27190  ppiublem1  27403  ppiublem2  27404  lgsdir2lem3  27528  gausslemma2dlem0i  27565  2lgs  27608  2lgsoddprmlem3  27615  2sqnn  27640  2sqreultblem  27649  2sqreunnltblem  27652  rpvmasum  27727  ltssolem1  27876  nulslts  28005  nulsgts  28006  vtxdg0v  29860  0enwwlksnge1  30250  rusgr0edg  30362  frgrreggt1  30781  topnfbey  30857  n0lpligALT  30873  isarchi  33533  constrmon  34165  sibf0  34756  signstfvneq0  34991  bnj98  35287  axnulALT2  35501  bisym1  36971  unqsym1  36977  bj-godellob  37239  poimirlem30  38342  axc5sp1  39738  areaquad  43984  cantnfresb  44092  succlg  44096  oacl2g  44098  omabs2  44100  omcl2  44101  fiiuncl  45826  iblempty  46720  vonhoire  47427  fveqvfvv  47818  ralndv1  47883  ndmaovcl  47981  mod2addne  48148  prmdvdsfmtnof1lem2  48378  31prm  48390  lighneallem3  48400  nprmdvdsfacm1lem2  48414  fpprbasnn  48535  sbgoldbaltlem1  48585  bgoldbtbndlem1  48611  stgr0  48766  upwlkbprop  48944  prmringnzring  49143