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  194  pm3.2ni  878  falim  1556  rex0  4292  rmo0  4294  0ss  4331  r19.2zb  4427  ral0OLD  4448  rabsnifsb  4659  snsssn  4773  axnulALT  5229  dtrucor  5295  axc16b  5313  iresn0n0  5966  elfv2ex  6824  brfvopab  7341  el2mpocsbcl  7934  bropopvvv  7939  bropfvvvv  7941  tfrlem16  8233  omordi  8406  nnmordi  8471  omabs  8490  omsmolem  8496  0er  8544  pssnn  8960  pssnnOLD  9049  fiint  9100  cantnfle  9438  r1sdom  9541  alephordi  9839  axdc3lem2  10216  canthp1  10419  elnnnn0b  12286  xltnegi  12959  xnn0xadd0  12990  xmulasslem2  13025  xrinf0  13081  elixx3g  13101  elfz2  13255  om2uzlti  13679  hashf1lem2  14179  relexpindlem  14783  sum0  15442  fsum2dlem  15491  prod0  15662  fprod2dlem  15699  nn0enne  16095  exprmfct  16418  prm23lt5  16524  4sqlem18  16672  vdwap0  16686  ram0  16732  prmlem1a  16817  prmlem2  16830  0catg  17406  dfgrp2e  18614  alexsub  23205  0met  23528  vitali  24786  plyeq0  25381  jensen  26147  ppiublem1  26359  ppiublem2  26360  lgsdir2lem3  26484  gausslemma2dlem0i  26521  2lgs  26564  2lgsoddprmlem3  26571  2sqnn  26596  2sqreultblem  26605  2sqreunnltblem  26608  rpvmasum  26683  vtxdg0v  27849  0enwwlksnge1  28238  rusgr0edg  28347  frgrreggt1  28766  topnfbey  28842  n0lpligALT  28855  isarchi  31445  sibf0  32310  sgn3da  32517  sgnnbi  32521  sgnpbi  32522  signstfvneq0  32560  bnj98  32856  sltsolem1  33887  nulsslt  34000  nulssgt  34001  bisym1  34617  unqsym1  34623  amosym1  34624  subsym1  34625  bj-godellob  34796  poimirlem30  35816  axc5sp1  36944  areaquad  41054  fiiuncl  42620  iblempty  43513  vonhoire  44217  fveqvfvv  44545  ralndv1  44608  ndmaovcl  44706  prmdvdsfmtnof1lem2  45048  31prm  45060  lighneallem3  45070  fpprbasnn  45192  sbgoldbaltlem1  45242  bgoldbtbndlem1  45268  upwlkbprop  45311