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  877  falim  1556  rex0  4356  rmo0  4358  0ss  4395  r19.2zb  4494  ral0OLD  4515  rabsnifsb  4725  snsssn  4841  axnulALT  5303  dtrucor  5368  axc16b  5386  iresn0n0  6052  elfv2ex  6936  brfvopab  7468  el2mpocsbcl  8073  bropopvvv  8078  bropfvvvv  8080  tfrlem16  8395  omordi  8568  nnmordi  8633  omabs  8652  omsmolem  8658  0er  8742  pssnn  9170  pssnnOLD  9267  fiint  9326  cantnfle  9668  r1sdom  9771  alephordi  10071  axdc3lem2  10448  canthp1  10651  elnnnn0b  12520  xltnegi  13199  xnn0xadd0  13230  xmulasslem2  13265  xrinf0  13321  elixx3g  13341  elfz2  13495  om2uzlti  13919  hashf1lem2  14421  relexpindlem  15014  sum0  15671  fsum2dlem  15720  prod0  15891  fprod2dlem  15928  nn0enne  16324  exprmfct  16645  prm23lt5  16751  4sqlem18  16899  vdwap0  16913  ram0  16959  prmlem1a  17044  prmlem2  17057  0catg  17636  dfgrp2e  18884  alexsub  23769  0met  24092  vitali  25362  plyeq0  25960  jensen  26729  ppiublem1  26941  ppiublem2  26942  lgsdir2lem3  27066  gausslemma2dlem0i  27103  2lgs  27146  2lgsoddprmlem3  27153  2sqnn  27178  2sqreultblem  27187  2sqreunnltblem  27190  rpvmasum  27265  sltsolem1  27414  nulsslt  27535  nulssgt  27536  vtxdg0v  28997  0enwwlksnge1  29385  rusgr0edg  29494  frgrreggt1  29913  topnfbey  29989  n0lpligALT  30004  isarchi  32598  sibf0  33631  sgn3da  33838  sgnnbi  33842  sgnpbi  33843  signstfvneq0  33881  bnj98  34176  bisym1  35607  unqsym1  35613  bj-godellob  35786  poimirlem30  36821  axc5sp1  38096  areaquad  42267  cantnfresb  42376  succlg  42380  oacl2g  42382  omabs2  42384  omcl2  42385  fiiuncl  44053  iblempty  44979  vonhoire  45686  fveqvfvv  46048  ralndv1  46111  ndmaovcl  46209  prmdvdsfmtnof1lem2  46551  31prm  46563  lighneallem3  46573  fpprbasnn  46695  sbgoldbaltlem1  46745  bgoldbtbndlem1  46771  upwlkbprop  46814