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  1556  rex0  4333  rmo0  4335  0ss  4373  r19.2zb  4469  rabsnifsb  4695  snsssn  4814  axnulALT  5271  dtrucor  5338  axc16b  5356  iresn0n0  6038  elfv2ex  6918  brfvopab  7458  el2mpocsbcl  8078  bropopvvv  8083  bropfvvvv  8085  tfrlem16  8401  omordi  8572  nnmordi  8637  omabs  8657  omsmolem  8663  0er  8751  pssnn  9176  fiint  9332  fiintOLD  9333  cantnfle  9677  r1sdom  9780  alephordi  10080  axdc3lem2  10457  canthp1  10660  elnnnn0b  12537  xltnegi  13224  xnn0xadd0  13255  xmulasslem2  13290  xrinf0  13346  elixx3g  13366  elfz2  13520  om2uzlti  13957  hashf1lem2  14462  hash3tpde  14499  relexpindlem  15069  sum0  15724  fsum2dlem  15773  prod0  15946  fprod2dlem  15983  nn0enne  16381  exprmfct  16708  prm23lt5  16819  4sqlem18  16967  vdwap0  16981  ram0  17027  prmlem1a  17111  prmlem2  17124  0catg  17685  dfgrp2e  18931  alexsub  23968  0met  24290  vitali  25551  plyeq0  26153  jensen  26935  ppiublem1  27149  ppiublem2  27150  lgsdir2lem3  27274  gausslemma2dlem0i  27311  2lgs  27354  2lgsoddprmlem3  27361  2sqnn  27386  2sqreultblem  27395  2sqreunnltblem  27398  rpvmasum  27473  sltsolem1  27623  nulsslt  27745  nulssgt  27746  vtxdg0v  29385  0enwwlksnge1  29778  rusgr0edg  29887  frgrreggt1  30306  topnfbey  30382  n0lpligALT  30397  isarchi  33098  constrmon  33694  sibf0  34274  sgn3da  34482  sgnnbi  34486  sgnpbi  34487  signstfvneq0  34525  bnj98  34819  bisym1  36358  unqsym1  36364  bj-godellob  36544  poimirlem30  37595  axc5sp1  38862  areaquad  43165  cantnfresb  43273  succlg  43277  oacl2g  43279  omabs2  43281  omcl2  43282  fiiuncl  45016  iblempty  45924  vonhoire  46631  fveqvfvv  46997  ralndv1  47062  ndmaovcl  47160  prmdvdsfmtnof1lem2  47517  31prm  47529  lighneallem3  47539  fpprbasnn  47661  sbgoldbaltlem1  47711  bgoldbtbndlem1  47737  uspgrimprop  47818  stgr0  47872  upwlkbprop  47999