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  4308  rmo0  4310  0ss  4350  rabsnifsb  4683  snsssn  4801  axnulALT  5258  dtrucor  5333  axc16b  5351  iresn0n0  6048  elfv2ex  6920  brfvopab  7469  el2mpocsbcl  8085  bropopvvv  8090  bropfvvvv  8092  tfrlem16  8385  omordi  8558  nnmordi  8624  omabs  8644  omsmolem  8650  0er  8740  pssnn  9168  fiint  9302  cantnfle  9656  r1sdom  9764  alephordi  10134  axdc3lem2  10510  canthp1  10720  elnnnn0b  12631  xltnegi  13327  xnn0xadd0  13358  xmulasslem2  13393  xrinf0  13450  elixx3g  13470  elfz2  13627  om2uzlti  14073  hashf1lem2  14581  hash3tpde  14618  relexpindlem  15196  sgn3da  15234  sgnnbi  15237  sgnpbi  15238  sum0  15867  fsum2dlem  15916  prod0  16090  fprod2dlem  16127  nn0enne  16527  exprmfct  16860  prm23lt5  16972  4sqlem18  17120  vdwap0  17134  ram0  17180  prmlem1a  17264  prmlem2  17278  0catg  17842  dfgrp2e  19154  alexsub  24344  0met  24665  vitali  25914  plyeq0  26510  jensen  27298  ppiublem1  27511  ppiublem2  27512  lgsdir2lem3  27636  gausslemma2dlem0i  27673  2lgs  27716  2lgsoddprmlem3  27723  2sqnn  27748  2sqreultblem  27757  2sqreunnltblem  27760  rpvmasum  27835  ltssolem1  28014  nulslts  28143  nulsgts  28144  vtxdg0v  30036  0enwwlksnge1  30435  rusgr0edg  30547  frgrreggt1  30976  topnfbey  31052  n0lpligALT  31068  isarchi  33725  constrmon  34358  sibf0  34949  signstfvneq0  35184  bnj98  35480  axnulALT2  35694  bisym1  37177  unqsym1  37183  bj-godellob  37445  poimirlem30  38536  axc5sp1  39948  areaquad  44176  cantnfresb  44284  succlg  44288  oacl2g  44290  omabs2  44292  omcl2  44293  fiiuncl  46025  iblempty  46919  vonhoire  47626  fveqvfvv  48054  ralndv1  48119  ndmaovcl  48217  mod2addne  48384  prmdvdsfmtnof1lem2  48614  31prm  48626  lighneallem3  48636  nprmdvdsfacm1lem2  48650  fpprbasnn  48771  sbgoldbaltlem1  48821  bgoldbtbndlem1  48847  stgr0  49002  upwlkbprop  49180  prmringnzring  49378