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  4326  rmo0  4328  0ss  4366  r19.2zb  4462  rabsnifsb  4689  snsssn  4808  axnulALT  5262  dtrucor  5329  axc16b  5347  iresn0n0  6028  elfv2ex  6907  brfvopab  7449  el2mpocsbcl  8067  bropopvvv  8072  bropfvvvv  8074  tfrlem16  8364  omordi  8533  nnmordi  8598  omabs  8618  omsmolem  8624  0er  8712  pssnn  9138  fiint  9284  fiintOLD  9285  cantnfle  9631  r1sdom  9734  alephordi  10034  axdc3lem2  10411  canthp1  10614  elnnnn0b  12493  xltnegi  13183  xnn0xadd0  13214  xmulasslem2  13249  xrinf0  13306  elixx3g  13326  elfz2  13482  om2uzlti  13922  hashf1lem2  14428  hash3tpde  14465  relexpindlem  15036  sum0  15694  fsum2dlem  15743  prod0  15916  fprod2dlem  15953  nn0enne  16354  exprmfct  16681  prm23lt5  16792  4sqlem18  16940  vdwap0  16954  ram0  17000  prmlem1a  17084  prmlem2  17097  0catg  17656  dfgrp2e  18902  alexsub  23939  0met  24261  vitali  25521  plyeq0  26123  jensen  26906  ppiublem1  27120  ppiublem2  27121  lgsdir2lem3  27245  gausslemma2dlem0i  27282  2lgs  27325  2lgsoddprmlem3  27332  2sqnn  27357  2sqreultblem  27366  2sqreunnltblem  27369  rpvmasum  27444  sltsolem1  27594  nulsslt  27716  nulssgt  27717  vtxdg0v  29408  0enwwlksnge1  29801  rusgr0edg  29910  frgrreggt1  30329  topnfbey  30405  n0lpligALT  30420  sgn3da  32766  sgnnbi  32770  sgnpbi  32771  isarchi  33143  constrmon  33741  sibf0  34332  signstfvneq0  34570  bnj98  34864  bisym1  36414  unqsym1  36420  bj-godellob  36600  poimirlem30  37651  axc5sp1  38923  areaquad  43212  cantnfresb  43320  succlg  43324  oacl2g  43326  omabs2  43328  omcl2  43329  fiiuncl  45066  iblempty  45970  vonhoire  46677  fveqvfvv  47045  ralndv1  47110  ndmaovcl  47208  mod2addne  47369  prmdvdsfmtnof1lem2  47590  31prm  47602  lighneallem3  47612  fpprbasnn  47734  sbgoldbaltlem1  47784  bgoldbtbndlem1  47810  stgr0  47963  upwlkbprop  48130