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  879  falim  1558  rex0  4322  rmo0  4324  0ss  4361  r19.2zb  4458  ral0OLD  4479  rabsnifsb  4688  snsssn  4804  axnulALT  5266  dtrucor  5331  axc16b  5349  iresn0n0  6012  elfv2ex  6893  brfvopab  7419  el2mpocsbcl  8022  bropopvvv  8027  bropfvvvv  8029  tfrlem16  8344  omordi  8518  nnmordi  8583  omabs  8602  omsmolem  8608  0er  8692  pssnn  9119  pssnnOLD  9216  fiint  9275  cantnfle  9616  r1sdom  9719  alephordi  10019  axdc3lem2  10396  canthp1  10599  elnnnn0b  12466  xltnegi  13145  xnn0xadd0  13176  xmulasslem2  13211  xrinf0  13267  elixx3g  13287  elfz2  13441  om2uzlti  13865  hashf1lem2  14367  relexpindlem  14960  sum0  15617  fsum2dlem  15666  prod0  15837  fprod2dlem  15874  nn0enne  16270  exprmfct  16591  prm23lt5  16697  4sqlem18  16845  vdwap0  16859  ram0  16905  prmlem1a  16990  prmlem2  17003  0catg  17582  dfgrp2e  18790  alexsub  23433  0met  23756  vitali  25014  plyeq0  25609  jensen  26375  ppiublem1  26587  ppiublem2  26588  lgsdir2lem3  26712  gausslemma2dlem0i  26749  2lgs  26792  2lgsoddprmlem3  26799  2sqnn  26824  2sqreultblem  26833  2sqreunnltblem  26836  rpvmasum  26911  sltsolem1  27060  nulsslt  27179  nulssgt  27180  vtxdg0v  28484  0enwwlksnge1  28872  rusgr0edg  28981  frgrreggt1  29400  topnfbey  29476  n0lpligALT  29489  isarchi  32088  sibf0  33023  sgn3da  33230  sgnnbi  33234  sgnpbi  33235  signstfvneq0  33273  bnj98  33568  bisym1  34967  unqsym1  34973  bj-godellob  35146  poimirlem30  36181  axc5sp1  37458  areaquad  41608  cantnfresb  41717  succlg  41721  oacl2g  41723  omabs2  41725  omcl2  41726  fiiuncl  43395  iblempty  44326  vonhoire  45033  fveqvfvv  45394  ralndv1  45457  ndmaovcl  45555  prmdvdsfmtnof1lem2  45897  31prm  45909  lighneallem3  45919  fpprbasnn  46041  sbgoldbaltlem1  46091  bgoldbtbndlem1  46117  upwlkbprop  46160