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  133  notnotriALT  134  pm2.21dd  197  pm3.2ni  877  falim  1554  rex0  4317  rmo0  4319  0ss  4350  r19.2zb  4441  ral0  4456  rabsnifsb  4658  snsssn  4772  axnulALT  5208  dtrucor  5272  axc16b  5290  iresn0n0  5923  elfv2ex  6711  brfvopab  7211  el2mpocsbcl  7780  bropopvvv  7785  bropfvvvv  7787  tfrlem16  8029  omordi  8192  nnmordi  8257  omabs  8274  omsmolem  8280  0er  8326  pssnn  8736  fiint  8795  cantnfle  9134  r1sdom  9203  alephordi  9500  axdc3lem2  9873  canthp1  10076  elnnnn0b  11942  xltnegi  12610  xnn0xadd0  12641  xmulasslem2  12676  xrinf0  12732  elixx3g  12752  elfz2  12900  om2uzlti  13319  hashf1lem2  13815  sum0  15078  fsum2dlem  15125  prod0  15297  fprod2dlem  15334  nn0enne  15728  exprmfct  16048  prm23lt5  16151  4sqlem18  16298  vdwap0  16312  ram0  16358  prmlem1a  16440  prmlem2  16453  0catg  16958  dfgrp2e  18129  alexsub  22653  0met  22976  vitali  24214  plyeq0  24801  jensen  25566  ppiublem1  25778  ppiublem2  25779  lgsdir2lem3  25903  gausslemma2dlem0i  25940  2lgs  25983  2lgsoddprmlem3  25990  2sqnn  26015  2sqreultblem  26024  2sqreunnltblem  26027  rpvmasum  26102  vtxdg0v  27255  0enwwlksnge1  27642  rusgr0edg  27752  frgrreggt1  28172  topnfbey  28248  n0lpligALT  28261  isarchi  30811  sibf0  31592  sgn3da  31799  sgnnbi  31803  sgnpbi  31804  signstfvneq0  31842  bnj98  32139  sltsolem1  33180  bisym1  33767  unqsym1  33773  amosym1  33774  subsym1  33775  bj-godellob  33939  poimirlem30  34937  axc5sp1  36074  areaquad  39872  fiiuncl  41376  iblempty  42299  vonhoire  43003  fveqvfvv  43324  ralndv1  43353  ndmaovcl  43451  prmdvdsfmtnof1lem2  43796  31prm  43809  lighneallem3  43821  fpprbasnn  43943  sbgoldbaltlem1  43993  bgoldbtbndlem1  44019  upwlkbprop  44062