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  133  notnotriALT  134  pm2.21dd  198  pm3.2ni  878  falim  1555  rex0  4271  rmo0  4273  0ss  4304  r19.2zb  4399  ral0  4414  rabsnifsb  4618  snsssn  4732  axnulALT  5172  dtrucor  5237  axc16b  5255  iresn0n0  5890  elfv2ex  6686  brfvopab  7190  el2mpocsbcl  7763  bropopvvv  7768  bropfvvvv  7770  tfrlem16  8012  omordi  8175  nnmordi  8240  omabs  8257  omsmolem  8263  0er  8309  pssnn  8720  fiint  8779  cantnfle  9118  r1sdom  9187  alephordi  9485  axdc3lem2  9862  canthp1  10065  elnnnn0b  11929  xltnegi  12597  xnn0xadd0  12628  xmulasslem2  12663  xrinf0  12719  elixx3g  12739  elfz2  12892  om2uzlti  13313  hashf1lem2  13810  relexpindlem  14414  sum0  15070  fsum2dlem  15117  prod0  15289  fprod2dlem  15326  nn0enne  15718  exprmfct  16038  prm23lt5  16141  4sqlem18  16288  vdwap0  16302  ram0  16348  prmlem1a  16432  prmlem2  16445  0catg  16950  dfgrp2e  18121  alexsub  22650  0met  22973  vitali  24217  plyeq0  24808  jensen  25574  ppiublem1  25786  ppiublem2  25787  lgsdir2lem3  25911  gausslemma2dlem0i  25948  2lgs  25991  2lgsoddprmlem3  25998  2sqnn  26023  2sqreultblem  26032  2sqreunnltblem  26035  rpvmasum  26110  vtxdg0v  27263  0enwwlksnge1  27650  rusgr0edg  27759  frgrreggt1  28178  topnfbey  28254  n0lpligALT  28267  isarchi  30861  sibf0  31702  sgn3da  31909  sgnnbi  31913  sgnpbi  31914  signstfvneq0  31952  bnj98  32249  sltsolem1  33293  bisym1  33880  unqsym1  33886  amosym1  33887  subsym1  33888  bj-godellob  34052  poimirlem30  35087  axc5sp1  36219  areaquad  40166  fiiuncl  41699  iblempty  42607  vonhoire  43311  fveqvfvv  43632  ralndv1  43661  ndmaovcl  43759  prmdvdsfmtnof1lem2  44102  31prm  44114  lighneallem3  44125  fpprbasnn  44247  sbgoldbaltlem1  44297  bgoldbtbndlem1  44323  upwlkbprop  44366