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  881  falim  1557  rex0  4360  rmo0  4362  0ss  4400  r19.2zb  4496  rabsnifsb  4722  snsssn  4841  axnulALT  5304  dtrucor  5371  axc16b  5389  iresn0n0  6072  elfv2ex  6952  brfvopab  7490  el2mpocsbcl  8110  bropopvvv  8115  bropfvvvv  8117  tfrlem16  8433  omordi  8604  nnmordi  8669  omabs  8689  omsmolem  8695  0er  8783  pssnn  9208  fiint  9366  fiintOLD  9367  cantnfle  9711  r1sdom  9814  alephordi  10114  axdc3lem2  10491  canthp1  10694  elnnnn0b  12570  xltnegi  13258  xnn0xadd0  13289  xmulasslem2  13324  xrinf0  13380  elixx3g  13400  elfz2  13554  om2uzlti  13991  hashf1lem2  14495  hash3tpde  14532  relexpindlem  15102  sum0  15757  fsum2dlem  15806  prod0  15979  fprod2dlem  16016  nn0enne  16414  exprmfct  16741  prm23lt5  16852  4sqlem18  17000  vdwap0  17014  ram0  17060  prmlem1a  17144  prmlem2  17157  0catg  17731  dfgrp2e  18981  alexsub  24053  0met  24376  vitali  25648  plyeq0  26250  jensen  27032  ppiublem1  27246  ppiublem2  27247  lgsdir2lem3  27371  gausslemma2dlem0i  27408  2lgs  27451  2lgsoddprmlem3  27458  2sqnn  27483  2sqreultblem  27492  2sqreunnltblem  27495  rpvmasum  27570  sltsolem1  27720  nulsslt  27842  nulssgt  27843  vtxdg0v  29491  0enwwlksnge1  29884  rusgr0edg  29993  frgrreggt1  30412  topnfbey  30488  n0lpligALT  30503  isarchi  33189  constrmon  33785  sibf0  34336  sgn3da  34544  sgnnbi  34548  sgnpbi  34549  signstfvneq0  34587  bnj98  34881  bisym1  36420  unqsym1  36426  bj-godellob  36606  poimirlem30  37657  axc5sp1  38924  areaquad  43228  cantnfresb  43337  succlg  43341  oacl2g  43343  omabs2  43345  omcl2  43346  fiiuncl  45070  iblempty  45980  vonhoire  46687  fveqvfvv  47052  ralndv1  47117  ndmaovcl  47215  prmdvdsfmtnof1lem2  47572  31prm  47584  lighneallem3  47594  fpprbasnn  47716  sbgoldbaltlem1  47766  bgoldbtbndlem1  47792  uspgrimprop  47873  stgr0  47927  upwlkbprop  48054