MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biimprd Unicode version

Theorem biimprd 214
Description: Deduce a converse implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 22-Sep-2013.)
Hypothesis
Ref Expression
biimprd.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
biimprd  |-  ( ph  ->  ( ch  ->  ps ) )

Proof of Theorem biimprd
StepHypRef Expression
1 id 19 . 2  |-  ( ch 
->  ch )
2 biimprd.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2syl5ibr 212 1  |-  ( ph  ->  ( ch  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  syl6bir  220  mpbird  223  sylibrd  225  sylbird  226  con4bid  284  mtbid  291  mtbii  293  imbi1d  308  biimpar  471  prlem1  928  spfw  1658  spw  1661  cbvalw  1676  cbvalvw  1677  alcomiw  1679  ax10lem2  1879  ax10lem4  1883  dral1  1908  cbval  1927  ax16i  1942  speiv  1945  sbequi  1998  sb9i  2033  a16g  2048  dral1-o  2095  a16g-o  2127  cleqh  2381  pm13.18  2519  rspcimdv  2886  rspcedv  2889  moi2  2947  moi  2949  sspsstr  3282  isso2i  4345  wefrc  4386  oneqmini  4442  ordsssuc2  4480  ordtri2or  4487  reusv6OLD  4544  reusv7OLD  4545  ralxfrd  4547  ralxfr2d  4549  orduniorsuc  4620  ordzsl  4635  tfinds  4649  elres  4989  sotri3  5072  2elresin  5321  f1ocnv  5451  tz6.12c  5509  fveqres  5522  fvun1  5552  dffo4  5638  fconst5  5693  isores3  5794  f1owe  5812  f1oweALT  5813  weniso  5814  ndmovordi  5973  fnse  6194  tposfo2  6219  issmo2  6362  iordsmo  6370  smoel2  6376  tz7.48lem  6449  abianfp  6467  oawordeulem  6548  om00  6569  omlimcl  6572  odi  6573  nnawordi  6615  fiint  7129  fipreima  7157  dffi2  7172  suplub2  7208  wemapso2lem  7261  unwdomg  7294  inf3lem3  7327  trcl  7406  fidomtri  7622  prdom2  7632  cardaleph  7712  ackbij1lem16  7857  coflim  7883  coftr  7895  infpssrlem4  7928  isfin7-2  8018  axdc3lem2  8073  axdc3lem4  8075  brdom6disj  8153  entric  8175  fpwwe2lem12  8259  inatsk  8396  grur1a  8437  indpi  8527  reclem3pr  8669  supsrlem  8729  lelttr  8908  fimaxre  9697  nnmulcl  9765  arch  9958  nnnegz  10023  zeo  10093  uzm1  10254  negn0  10300  rpneg  10379  xrlttri  10469  xrlelttr  10483  iccid  10697  icoshft  10754  fzen  10807  elfz2nn0  10817  fzm1  10858  max0add  11791  abslt  11794  absle  11795  rexuzre  11832  caurcvg  12145  caucvg  12147  dvdsval2  12530  negdvdsb  12541  muldvds2  12550  smuval2  12669  smupvallem  12670  rplpwr  12731  alginv  12741  algfx  12746  rpexp1i  12796  qnumdencl  12806  phiprmpw  12840  prmdiveq  12850  pcmpt  12936  infpnlem1  12953  imasaddfnlem  13426  plelttr  14102  lubid  14112  mndodconglem  14852  cnpnei  16989  uncon  17151  kqsat  17418  isr0  17424  qtophmeo  17504  trufil  17601  alexsubALT  17741  bl2in  17953  addcnlem  18364  rescncf  18397  ovoliunlem2  18858  voliun  18907  mbflimsup  19017  itgcn  19193  dvdsq1p  19542  aalioulem2  19709  recosf1o  19893  logrec  20113  xrlimcnp  20259  basellem4  20317  bposlem1  20519  bposlem5  20523  lgsdchrval  20582  pntlem3  20754  elghomlem2  21023  blocn2  21380  htthlem  21491  axhcompl-zf  21574  spanuni  22119  spansncol  22143  spansneleq  22145  elspansn5  22149  idcnop  22557  pjnormssi  22744  dmdmd  22876  ifeqeqx  23030  erdsze2lem2  23142  cvmsval  23204  eupai  23290  ghomgsg  23407  ghomf1olem  23408  dedekindle  23489  fundmpss  23526  dfon2lem3  23545  frmin  23646  poseq  23657  soseq  23658  wfrlem5  23664  wfrlem10  23669  wfrlem12  23671  frrlem5  23689  frrlem11  23697  axfelem9  23758  axfelem10  23759  axfelem16  23765  dfrdg4  23898  brbtwn2  23943  axbtwnid  23977  cgrtriv  24035  btwntriv2  24045  ifscgr  24077  lineext  24109  btwnconn1lem12  24131  colinbtwnle  24151  ontgval  24280  onsucconi  24286  areacirclem4  24337  areacirclem6  24340  areacirc  24341  boxbid  24421  nxtbid  24422  diabid  24423  untbi12d  24432  cbicp  24577  prodeq3ii  24719  dffprod  24730  ablocomgrp  24753  abhp  25584  elicc3  25639  comppfsc  25718  nninfnub  25872  prdstotbnd  25929  heiborlem4  25949  heibor  25956  grpokerinj  25986  isidlc  26051  prtlem17  26155  elrfirn2  26182  rencldnfilem  26314  sdrgacs  26920  stoweidlem18  27178  stoweidlem27  27187  stoweidlem35  27195  stoweidlem48  27208  rexrsb  27338  funbrafv  27411  snelpwrVD  27886  en3lplem1VD  27899  en3lpVD  27901  orbi1rVD  27904  sbc3orgVD  27907  3impexpVD  27912  equncomVD  27924  trsbcVD  27933  trintALTVD  27936  trintALT  27937  csbingVD  27940  csbsngVD  27949  csbxpgVD  27950  csbrngVD  27952  csbfv12gALTVD  27955  relopabVD  27957  e2ebindVD  27968  bnj580  28224  ax10lem18ALT  28403  lsator0sp  28470  atlrelat1  28790  cvratlem  28889  diaintclN  30527  dibintclN  30636  cdlemn11pre  30679  dihord2pre  30694  dihintcl  30813  dochkrshp4  30858  lcfrlem9  31019  lcfrlem21  31032  mapdh8e  31253
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator