MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.21i Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 pm2.21i.1 . . 3 ¬ 𝜑
21a1i 11 . 2 𝜓 → ¬ 𝜑)
32con4i 114 1 (𝜑𝜓)
Colors of variables: wff setvar class
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  197  pm3.2ni  876  falim  1547  rex0  4315  rmo0  4317  0ss  4348  r19.2zb  4439  ral0  4454  rabsnifsb  4650  snsssn  4764  axnulALT  5199  dtrucor  5263  axc16b  5280  iresn0n0  5916  elfv2ex  6704  brfvopab  7203  el2mpocsbcl  7772  bropopvvv  7777  bropfvvvv  7779  tfrlem16  8021  omordi  8184  nnmordi  8249  omabs  8266  omsmolem  8272  0er  8318  pssnn  8728  fiint  8787  cantnfle  9126  r1sdom  9195  alephordi  9492  axdc3lem2  9865  canthp1  10068  elnnnn0b  11933  xltnegi  12601  xnn0xadd0  12632  xmulasslem2  12667  xrinf0  12723  elixx3g  12743  elfz2  12891  om2uzlti  13310  hashf1lem2  13806  sum0  15070  fsum2dlem  15117  prod0  15289  fprod2dlem  15326  nn0enne  15720  exprmfct  16040  prm23lt5  16143  4sqlem18  16290  vdwap0  16304  ram0  16350  prmlem1a  16432  prmlem2  16445  0catg  16950  dfgrp2e  18121  alexsub  22645  0met  22968  vitali  24206  plyeq0  24793  jensen  25558  ppiublem1  25770  ppiublem2  25771  lgsdir2lem3  25895  gausslemma2dlem0i  25932  2lgs  25975  2lgsoddprmlem3  25982  2sqnn  26007  2sqreultblem  26016  2sqreunnltblem  26019  rpvmasum  26094  vtxdg0v  27247  0enwwlksnge1  27634  rusgr0edg  27744  frgrreggt1  28164  topnfbey  28240  n0lpligALT  28253  isarchi  30804  sibf0  31580  sgn3da  31787  sgnnbi  31791  sgnpbi  31792  signstfvneq0  31830  bnj98  32127  sltsolem1  33168  bisym1  33755  unqsym1  33761  amosym1  33762  subsym1  33763  bj-godellob  33927  poimirlem30  34909  axc5sp1  36046  areaquad  39808  fiiuncl  41312  iblempty  42234  vonhoire  42939  fveqvfvv  43260  ralndv1  43289  ndmaovcl  43387  prmdvdsfmtnof1lem2  43732  31prm  43745  lighneallem3  43757  fpprbasnn  43879  sbgoldbaltlem1  43929  bgoldbtbndlem1  43955  upwlkbprop  43998
  Copyright terms: Public domain W3C validator