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 116
Description: A contradiction implies anything. Inference associated with pm2.21 120. Its associated inference is pm2.24ii 117. (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 113 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  117  notnotri  126  pm2.21dd  186  pm3.2ni  917  annotanannotOLD  960  falim  1538  nfnthOLD  1776  rex0  3971  0ss  4005  r19.2zb  4094  ral0  4109  rabsnifsb  4289  snsssn  4404  int0OLD  4523  axnulALT  4820  axc16b  4888  dtrucor  4930  elfv2ex  6267  brfvopab  6742  el2mpt2csbcl  7295  bropopvvv  7300  bropfvvvv  7302  tfrlem16  7534  omordi  7691  nnmordi  7756  omabs  7772  omsmolem  7778  0er  7824  pssnn  8219  fiint  8278  cantnfle  8606  r1sdom  8675  alephordi  8935  axdc3lem2  9311  canthp1  9514  elnnnn0b  11375  xltnegi  12085  xnn0xadd0  12115  xmulasslem2  12150  xrinf0  12206  elixx3g  12226  elfz2  12371  om2uzlti  12789  hashf1lem2  13278  sum0  14496  fsum2dlem  14545  prod0  14717  fprod2dlem  14754  nn0enne  15141  exprmfct  15463  prm23lt5  15566  4sqlem18  15713  vdwap0  15727  ram0  15773  prmlem1a  15860  prmlem2  15874  xpsfrnel2  16272  0catg  16395  dfgrp2e  17495  alexsub  21896  0met  22218  vitali  23427  plyeq0  24012  jensen  24760  ppiublem1  24972  ppiublem2  24973  lgsdir2lem3  25097  gausslemma2dlem0i  25134  2lgs  25177  2lgsoddprmlem3  25184  rpvmasum  25260  vtxdg0v  26425  0enwwlksnge1  26818  rusgr0edg  26940  frgrreggt1  27380  topnfbey  27455  n0lpligALT  27466  isarchi  29864  sibf0  30524  sgn3da  30731  sgnnbi  30735  sgnpbi  30736  signstfvneq0  30777  bnj98  31063  sltsolem1  31951  bisym1  32543  unqsym1  32549  amosym1  32550  subsym1  32551  bj-godellob  32715  bj-axc16b  32923  bj-dtrucor  32925  poimirlem30  33569  axc5sp1  34527  areaquad  38119  fiiuncl  39548  iblempty  40499  vonhoire  41207  fveqvfvv  41525  ndmaovcl  41604  prmdvdsfmtnof1lem2  41822  31prm  41837  lighneallem3  41849  sbgoldbaltlem1  41992  bgoldbtbndlem1  42018  upwlkbprop  42044
  Copyright terms: Public domain W3C validator