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  4313  rmo0  4315  0ss  4353  r19.2zb  4449  rabsnifsb  4676  snsssn  4795  axnulALT  5246  dtrucor  5313  axc16b  5331  iresn0n0  6009  elfv2ex  6870  brfvopab  7410  el2mpocsbcl  8025  bropopvvv  8030  bropfvvvv  8032  tfrlem16  8322  omordi  8491  nnmordi  8556  omabs  8576  omsmolem  8582  0er  8670  pssnn  9092  fiint  9235  fiintOLD  9236  cantnfle  9586  r1sdom  9689  alephordi  9987  axdc3lem2  10364  canthp1  10567  elnnnn0b  12446  xltnegi  13136  xnn0xadd0  13167  xmulasslem2  13202  xrinf0  13259  elixx3g  13279  elfz2  13435  om2uzlti  13875  hashf1lem2  14381  hash3tpde  14418  relexpindlem  14988  sum0  15646  fsum2dlem  15695  prod0  15868  fprod2dlem  15905  nn0enne  16306  exprmfct  16633  prm23lt5  16744  4sqlem18  16892  vdwap0  16906  ram0  16952  prmlem1a  17036  prmlem2  17049  0catg  17612  dfgrp2e  18860  alexsub  23948  0met  24270  vitali  25530  plyeq0  26132  jensen  26915  ppiublem1  27129  ppiublem2  27130  lgsdir2lem3  27254  gausslemma2dlem0i  27291  2lgs  27334  2lgsoddprmlem3  27341  2sqnn  27366  2sqreultblem  27375  2sqreunnltblem  27378  rpvmasum  27453  sltsolem1  27603  nulsslt  27726  nulssgt  27727  vtxdg0v  29437  0enwwlksnge1  29827  rusgr0edg  29936  frgrreggt1  30355  topnfbey  30431  n0lpligALT  30446  sgn3da  32792  sgnnbi  32796  sgnpbi  32797  isarchi  33134  constrmon  33710  sibf0  34301  signstfvneq0  34539  bnj98  34833  bisym1  36392  unqsym1  36398  bj-godellob  36578  poimirlem30  37629  axc5sp1  38901  areaquad  43189  cantnfresb  43297  succlg  43301  oacl2g  43303  omabs2  43305  omcl2  43306  fiiuncl  45043  iblempty  45947  vonhoire  46654  fveqvfvv  47025  ralndv1  47090  ndmaovcl  47188  mod2addne  47349  prmdvdsfmtnof1lem2  47570  31prm  47582  lighneallem3  47592  fpprbasnn  47714  sbgoldbaltlem1  47764  bgoldbtbndlem1  47790  stgr0  47943  upwlkbprop  48110