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  194  pm3.2ni  880  falim  1559  rex0  4358  rmo0  4360  0ss  4397  r19.2zb  4496  ral0OLD  4517  rabsnifsb  4727  snsssn  4843  axnulALT  5305  dtrucor  5370  axc16b  5388  iresn0n0  6054  elfv2ex  6938  brfvopab  7466  el2mpocsbcl  8071  bropopvvv  8076  bropfvvvv  8078  tfrlem16  8393  omordi  8566  nnmordi  8631  omabs  8650  omsmolem  8656  0er  8740  pssnn  9168  pssnnOLD  9265  fiint  9324  cantnfle  9666  r1sdom  9769  alephordi  10069  axdc3lem2  10446  canthp1  10649  elnnnn0b  12516  xltnegi  13195  xnn0xadd0  13226  xmulasslem2  13261  xrinf0  13317  elixx3g  13337  elfz2  13491  om2uzlti  13915  hashf1lem2  14417  relexpindlem  15010  sum0  15667  fsum2dlem  15716  prod0  15887  fprod2dlem  15924  nn0enne  16320  exprmfct  16641  prm23lt5  16747  4sqlem18  16895  vdwap0  16909  ram0  16955  prmlem1a  17040  prmlem2  17053  0catg  17632  dfgrp2e  18848  alexsub  23549  0met  23872  vitali  25130  plyeq0  25725  jensen  26493  ppiublem1  26705  ppiublem2  26706  lgsdir2lem3  26830  gausslemma2dlem0i  26867  2lgs  26910  2lgsoddprmlem3  26917  2sqnn  26942  2sqreultblem  26951  2sqreunnltblem  26954  rpvmasum  27029  sltsolem1  27178  nulsslt  27298  nulssgt  27299  vtxdg0v  28730  0enwwlksnge1  29118  rusgr0edg  29227  frgrreggt1  29646  topnfbey  29722  n0lpligALT  29737  isarchi  32328  sibf0  33333  sgn3da  33540  sgnnbi  33544  sgnpbi  33545  signstfvneq0  33583  bnj98  33878  bisym1  35304  unqsym1  35310  bj-godellob  35483  poimirlem30  36518  axc5sp1  37793  areaquad  41965  cantnfresb  42074  succlg  42078  oacl2g  42080  omabs2  42082  omcl2  42083  fiiuncl  43752  iblempty  44681  vonhoire  45388  fveqvfvv  45750  ralndv1  45813  ndmaovcl  45911  prmdvdsfmtnof1lem2  46253  31prm  46265  lighneallem3  46275  fpprbasnn  46397  sbgoldbaltlem1  46447  bgoldbtbndlem1  46473  upwlkbprop  46516