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  877  falim  1556  rex0  4288  rmo0  4290  0ss  4327  r19.2zb  4423  ral0OLD  4444  rabsnifsb  4655  snsssn  4769  axnulALT  5223  dtrucor  5289  axc16b  5307  iresn0n0  5952  elfv2ex  6797  brfvopab  7310  el2mpocsbcl  7896  bropopvvv  7901  bropfvvvv  7903  tfrlem16  8195  omordi  8359  nnmordi  8424  omabs  8441  omsmolem  8447  0er  8493  pssnn  8913  pssnnOLD  8969  fiint  9021  cantnfle  9359  r1sdom  9463  alephordi  9761  axdc3lem2  10138  canthp1  10341  elnnnn0b  12207  xltnegi  12879  xnn0xadd0  12910  xmulasslem2  12945  xrinf0  13001  elixx3g  13021  elfz2  13175  om2uzlti  13598  hashf1lem2  14098  relexpindlem  14702  sum0  15361  fsum2dlem  15410  prod0  15581  fprod2dlem  15618  nn0enne  16014  exprmfct  16337  prm23lt5  16443  4sqlem18  16591  vdwap0  16605  ram0  16651  prmlem1a  16736  prmlem2  16749  0catg  17314  dfgrp2e  18520  alexsub  23104  0met  23427  vitali  24682  plyeq0  25277  jensen  26043  ppiublem1  26255  ppiublem2  26256  lgsdir2lem3  26380  gausslemma2dlem0i  26417  2lgs  26460  2lgsoddprmlem3  26467  2sqnn  26492  2sqreultblem  26501  2sqreunnltblem  26504  rpvmasum  26579  vtxdg0v  27743  0enwwlksnge1  28130  rusgr0edg  28239  frgrreggt1  28658  topnfbey  28734  n0lpligALT  28747  isarchi  31338  sibf0  32201  sgn3da  32408  sgnnbi  32412  sgnpbi  32413  signstfvneq0  32451  bnj98  32747  sltsolem1  33805  nulsslt  33918  nulssgt  33919  bisym1  34535  unqsym1  34541  amosym1  34542  subsym1  34543  bj-godellob  34714  poimirlem30  35734  axc5sp1  36864  areaquad  40963  fiiuncl  42502  iblempty  43396  vonhoire  44100  fveqvfvv  44421  ralndv1  44484  ndmaovcl  44582  prmdvdsfmtnof1lem2  44925  31prm  44937  lighneallem3  44947  fpprbasnn  45069  sbgoldbaltlem1  45119  bgoldbtbndlem1  45145  upwlkbprop  45188