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  880  falim  1557  rex0  4323  rmo0  4325  0ss  4363  r19.2zb  4459  rabsnifsb  4686  snsssn  4805  axnulALT  5259  dtrucor  5326  axc16b  5344  iresn0n0  6025  elfv2ex  6904  brfvopab  7446  el2mpocsbcl  8064  bropopvvv  8069  bropfvvvv  8071  tfrlem16  8361  omordi  8530  nnmordi  8595  omabs  8615  omsmolem  8621  0er  8709  pssnn  9132  fiint  9277  fiintOLD  9278  cantnfle  9624  r1sdom  9727  alephordi  10027  axdc3lem2  10404  canthp1  10607  elnnnn0b  12486  xltnegi  13176  xnn0xadd0  13207  xmulasslem2  13242  xrinf0  13299  elixx3g  13319  elfz2  13475  om2uzlti  13915  hashf1lem2  14421  hash3tpde  14458  relexpindlem  15029  sum0  15687  fsum2dlem  15736  prod0  15909  fprod2dlem  15946  nn0enne  16347  exprmfct  16674  prm23lt5  16785  4sqlem18  16933  vdwap0  16947  ram0  16993  prmlem1a  17077  prmlem2  17090  0catg  17649  dfgrp2e  18895  alexsub  23932  0met  24254  vitali  25514  plyeq0  26116  jensen  26899  ppiublem1  27113  ppiublem2  27114  lgsdir2lem3  27238  gausslemma2dlem0i  27275  2lgs  27318  2lgsoddprmlem3  27325  2sqnn  27350  2sqreultblem  27359  2sqreunnltblem  27362  rpvmasum  27437  sltsolem1  27587  nulsslt  27709  nulssgt  27710  vtxdg0v  29401  0enwwlksnge1  29794  rusgr0edg  29903  frgrreggt1  30322  topnfbey  30398  n0lpligALT  30413  sgn3da  32759  sgnnbi  32763  sgnpbi  32764  isarchi  33136  constrmon  33734  sibf0  34325  signstfvneq0  34563  bnj98  34857  bisym1  36407  unqsym1  36413  bj-godellob  36593  poimirlem30  37644  axc5sp1  38916  areaquad  43205  cantnfresb  43313  succlg  43317  oacl2g  43319  omabs2  43321  omcl2  43322  fiiuncl  45059  iblempty  45963  vonhoire  46670  fveqvfvv  47041  ralndv1  47106  ndmaovcl  47204  mod2addne  47365  prmdvdsfmtnof1lem2  47586  31prm  47598  lighneallem3  47608  fpprbasnn  47730  sbgoldbaltlem1  47780  bgoldbtbndlem1  47806  stgr0  47959  upwlkbprop  48126