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  1557  rex0  4335  rmo0  4337  0ss  4375  r19.2zb  4471  rabsnifsb  4698  snsssn  4817  axnulALT  5274  dtrucor  5341  axc16b  5359  iresn0n0  6041  elfv2ex  6922  brfvopab  7464  el2mpocsbcl  8084  bropopvvv  8089  bropfvvvv  8091  tfrlem16  8407  omordi  8578  nnmordi  8643  omabs  8663  omsmolem  8669  0er  8757  pssnn  9182  fiint  9338  fiintOLD  9339  cantnfle  9685  r1sdom  9788  alephordi  10088  axdc3lem2  10465  canthp1  10668  elnnnn0b  12545  xltnegi  13232  xnn0xadd0  13263  xmulasslem2  13298  xrinf0  13355  elixx3g  13375  elfz2  13531  om2uzlti  13968  hashf1lem2  14474  hash3tpde  14511  relexpindlem  15082  sum0  15737  fsum2dlem  15786  prod0  15959  fprod2dlem  15996  nn0enne  16396  exprmfct  16723  prm23lt5  16834  4sqlem18  16982  vdwap0  16996  ram0  17042  prmlem1a  17126  prmlem2  17139  0catg  17700  dfgrp2e  18946  alexsub  23983  0met  24305  vitali  25566  plyeq0  26168  jensen  26951  ppiublem1  27165  ppiublem2  27166  lgsdir2lem3  27290  gausslemma2dlem0i  27327  2lgs  27370  2lgsoddprmlem3  27377  2sqnn  27402  2sqreultblem  27411  2sqreunnltblem  27414  rpvmasum  27489  sltsolem1  27639  nulsslt  27761  nulssgt  27762  vtxdg0v  29453  0enwwlksnge1  29846  rusgr0edg  29955  frgrreggt1  30374  topnfbey  30450  n0lpligALT  30465  sgn3da  32813  sgnnbi  32817  sgnpbi  32818  isarchi  33180  constrmon  33778  sibf0  34366  signstfvneq0  34604  bnj98  34898  bisym1  36437  unqsym1  36443  bj-godellob  36623  poimirlem30  37674  axc5sp1  38941  areaquad  43240  cantnfresb  43348  succlg  43352  oacl2g  43354  omabs2  43356  omcl2  43357  fiiuncl  45089  iblempty  45994  vonhoire  46701  fveqvfvv  47069  ralndv1  47134  ndmaovcl  47232  prmdvdsfmtnof1lem2  47599  31prm  47611  lighneallem3  47621  fpprbasnn  47743  sbgoldbaltlem1  47793  bgoldbtbndlem1  47819  stgr0  47972  upwlkbprop  48113