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  197  pm3.2ni  891  falim  1576  rex0  4312  rmo0  4314  0ss  4353  rabsnifsb  4680  snsssn  4798  axnulALT  5253  dtrucor  5327  axc16b  5345  iresn0n0  6040  elfv2ex  6906  brfvopab  7449  el2mpocsbcl  8059  bropopvvv  8064  bropfvvvv  8066  tfrlem16  8359  omordi  8530  nnmordi  8596  omabs  8616  omsmolem  8622  0er  8712  pssnn  9133  fiint  9267  cantnfle  9623  r1sdom  9729  alephordi  10027  axdc3lem2  10405  canthp1  10609  elnnnn0b  12522  xltnegi  13216  xnn0xadd0  13247  xmulasslem2  13282  xrinf0  13339  elixx3g  13359  elfz2  13516  om2uzlti  13960  hashf1lem2  14466  hash3tpde  14503  relexpindlem  15073  sum0  15731  fsum2dlem  15780  prod0  15956  fprod2dlem  15993  nn0enne  16394  exprmfct  16722  prm23lt5  16833  4sqlem18  16981  vdwap0  16995  ram0  17041  prmlem1a  17125  prmlem2  17139  0catg  17703  dfgrp2e  18988  alexsub  24085  0met  24406  vitali  25655  plyeq0  26251  jensen  27030  ppiublem1  27243  ppiublem2  27244  lgsdir2lem3  27368  gausslemma2dlem0i  27405  2lgs  27448  2lgsoddprmlem3  27455  2sqnn  27480  2sqreultblem  27489  2sqreunnltblem  27492  rpvmasum  27567  ltssolem1  27716  nulslts  27845  nulsgts  27846  vtxdg0v  29620  0enwwlksnge1  30010  rusgr0edg  30122  frgrreggt1  30541  topnfbey  30617  n0lpligALT  30633  sgn3da  32986  sgnnbi  32990  sgnpbi  32991  isarchi  33323  constrmon  34002  sibf0  34592  signstfvneq0  34830  bnj98  35126  axnulALT2  35341  bisym1  36743  unqsym1  36749  bj-godellob  37012  poimirlem30  38113  axc5sp1  39511  areaquad  43757  cantnfresb  43865  succlg  43869  oacl2g  43871  omabs2  43873  omcl2  43874  fiiuncl  45609  iblempty  46503  vonhoire  47210  fveqvfvv  47598  ralndv1  47663  ndmaovcl  47761  mod2addne  47928  prmdvdsfmtnof1lem2  48158  31prm  48170  lighneallem3  48180  nprmdvdsfacm1lem2  48194  fpprbasnn  48315  sbgoldbaltlem1  48365  bgoldbtbndlem1  48391  stgr0  48546  upwlkbprop  48724