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  195  pm3.2ni  880  falim  1558  rex0  4308  rmo0  4310  0ss  4348  r19.2zb  4444  rabsnifsb  4673  snsssn  4791  axnulALT  5240  dtrucor  5307  axc16b  5325  iresn0n0  6000  elfv2ex  6860  brfvopab  7398  el2mpocsbcl  8010  bropopvvv  8015  bropfvvvv  8017  tfrlem16  8307  omordi  8476  nnmordi  8541  omabs  8561  omsmolem  8567  0er  8655  pssnn  9073  fiint  9206  cantnfle  9556  r1sdom  9659  alephordi  9957  axdc3lem2  10334  canthp1  10537  elnnnn0b  12417  xltnegi  13107  xnn0xadd0  13138  xmulasslem2  13173  xrinf0  13230  elixx3g  13250  elfz2  13406  om2uzlti  13849  hashf1lem2  14355  hash3tpde  14392  relexpindlem  14962  sum0  15620  fsum2dlem  15669  prod0  15842  fprod2dlem  15879  nn0enne  16280  exprmfct  16607  prm23lt5  16718  4sqlem18  16866  vdwap0  16880  ram0  16926  prmlem1a  17010  prmlem2  17023  0catg  17586  dfgrp2e  18868  alexsub  23953  0met  24274  vitali  25534  plyeq0  26136  jensen  26919  ppiublem1  27133  ppiublem2  27134  lgsdir2lem3  27258  gausslemma2dlem0i  27295  2lgs  27338  2lgsoddprmlem3  27345  2sqnn  27370  2sqreultblem  27379  2sqreunnltblem  27382  rpvmasum  27457  sltsolem1  27607  nulsslt  27731  nulssgt  27732  vtxdg0v  29445  0enwwlksnge1  29835  rusgr0edg  29944  frgrreggt1  30363  topnfbey  30439  n0lpligALT  30454  sgn3da  32807  sgnnbi  32811  sgnpbi  32812  isarchi  33141  constrmon  33747  sibf0  34337  signstfvneq0  34575  bnj98  34869  bisym1  36432  unqsym1  36438  bj-godellob  36618  poimirlem30  37669  axc5sp1  38941  areaquad  43228  cantnfresb  43336  succlg  43340  oacl2g  43342  omabs2  43344  omcl2  43345  fiiuncl  45081  iblempty  45982  vonhoire  46689  fveqvfvv  47050  ralndv1  47115  ndmaovcl  47213  mod2addne  47374  prmdvdsfmtnof1lem2  47595  31prm  47607  lighneallem3  47617  fpprbasnn  47739  sbgoldbaltlem1  47789  bgoldbtbndlem1  47815  stgr0  47970  upwlkbprop  48148