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  1559  rex0  4300  rmo0  4302  0ss  4340  rabsnifsb  4666  snsssn  4784  axnulALT  5239  dtrucor  5313  axc16b  5331  iresn0n0  6019  elfv2ex  6883  brfvopab  7424  el2mpocsbcl  8035  bropopvvv  8040  bropfvvvv  8042  tfrlem16  8332  omordi  8501  nnmordi  8567  omabs  8587  omsmolem  8593  0er  8682  pssnn  9103  fiint  9237  cantnfle  9592  r1sdom  9698  alephordi  9996  axdc3lem2  10373  canthp1  10577  elnnnn0b  12481  xltnegi  13168  xnn0xadd0  13199  xmulasslem2  13234  xrinf0  13291  elixx3g  13311  elfz2  13468  om2uzlti  13912  hashf1lem2  14418  hash3tpde  14455  relexpindlem  15025  sum0  15683  fsum2dlem  15732  prod0  15908  fprod2dlem  15945  nn0enne  16346  exprmfct  16674  prm23lt5  16785  4sqlem18  16933  vdwap0  16947  ram0  16993  prmlem1a  17077  prmlem2  17090  0catg  17654  dfgrp2e  18939  alexsub  24010  0met  24331  vitali  25580  plyeq0  26176  jensen  26952  ppiublem1  27165  ppiublem2  27166  lgsdir2lem3  27290  gausslemma2dlem0i  27327  2lgs  27370  2lgsoddprmlem3  27377  2sqnn  27402  2sqreultblem  27411  2sqreunnltblem  27414  rpvmasum  27489  ltssolem1  27639  nulslts  27767  nulsgts  27768  vtxdg0v  29542  0enwwlksnge1  29932  rusgr0edg  30044  frgrreggt1  30463  topnfbey  30539  n0lpligALT  30555  sgn3da  32907  sgnnbi  32911  sgnpbi  32912  isarchi  33243  constrmon  33888  sibf0  34478  signstfvneq0  34716  bnj98  35009  axnulALT2  35224  bisym1  36601  unqsym1  36607  bj-godellob  36870  poimirlem30  37971  axc5sp1  39369  areaquad  43644  cantnfresb  43752  succlg  43756  oacl2g  43758  omabs2  43760  omcl2  43761  fiiuncl  45496  iblempty  46393  vonhoire  47100  fveqvfvv  47488  ralndv1  47553  ndmaovcl  47651  mod2addne  47818  prmdvdsfmtnof1lem2  48048  31prm  48060  lighneallem3  48070  nprmdvdsfacm1lem2  48084  fpprbasnn  48205  sbgoldbaltlem1  48255  bgoldbtbndlem1  48281  stgr0  48436  upwlkbprop  48614