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  4311  rmo0  4313  0ss  4351  r19.2zb  4447  rabsnifsb  4676  snsssn  4794  axnulALT  5246  dtrucor  5313  axc16b  5331  iresn0n0  6010  elfv2ex  6874  brfvopab  7412  el2mpocsbcl  8024  bropopvvv  8029  bropfvvvv  8031  tfrlem16  8321  omordi  8490  nnmordi  8555  omabs  8575  omsmolem  8581  0er  8669  pssnn  9088  fiint  9221  cantnfle  9571  r1sdom  9677  alephordi  9975  axdc3lem2  10352  canthp1  10555  elnnnn0b  12435  xltnegi  13125  xnn0xadd0  13156  xmulasslem2  13191  xrinf0  13248  elixx3g  13268  elfz2  13424  om2uzlti  13867  hashf1lem2  14373  hash3tpde  14410  relexpindlem  14980  sum0  15638  fsum2dlem  15687  prod0  15860  fprod2dlem  15897  nn0enne  16298  exprmfct  16625  prm23lt5  16736  4sqlem18  16884  vdwap0  16898  ram0  16944  prmlem1a  17028  prmlem2  17041  0catg  17604  dfgrp2e  18886  alexsub  23970  0met  24291  vitali  25551  plyeq0  26153  jensen  26936  ppiublem1  27150  ppiublem2  27151  lgsdir2lem3  27275  gausslemma2dlem0i  27312  2lgs  27355  2lgsoddprmlem3  27362  2sqnn  27387  2sqreultblem  27396  2sqreunnltblem  27399  rpvmasum  27474  sltsolem1  27624  nulsslt  27748  nulssgt  27749  vtxdg0v  29463  0enwwlksnge1  29853  rusgr0edg  29965  frgrreggt1  30384  topnfbey  30460  n0lpligALT  30475  sgn3da  32828  sgnnbi  32832  sgnpbi  32833  isarchi  33162  constrmon  33768  sibf0  34358  signstfvneq0  34596  bnj98  34890  bisym1  36474  unqsym1  36480  bj-godellob  36660  poimirlem30  37700  axc5sp1  39032  areaquad  43323  cantnfresb  43431  succlg  43435  oacl2g  43437  omabs2  43439  omcl2  43440  fiiuncl  45176  iblempty  46077  vonhoire  46784  fveqvfvv  47154  ralndv1  47219  ndmaovcl  47317  mod2addne  47478  prmdvdsfmtnof1lem2  47699  31prm  47711  lighneallem3  47721  fpprbasnn  47843  sbgoldbaltlem1  47893  bgoldbtbndlem1  47919  stgr0  48074  upwlkbprop  48252