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  1696  spw  1699  cbvalw  1706  cbvalvw  1707  alcomiw  1709  nfimd  1815  ax10lem2  1950  ax10lem4  1954  dral1  1978  cbval  1997  speiv  2013  ax16i  2059  a16gALT  2062  sbequi  2072  sb9i  2107  dral1-o  2167  a16g-o  2199  cleqh  2463  pm13.18  2601  rspcimdv  2970  rspcedv  2973  moi2  3032  moi  3034  sspsstr  3368  isso2i  4449  wefrc  4490  oneqmini  4546  ordsssuc2  4584  ordtri2or  4591  reusv6OLD  4648  reusv7OLD  4649  ralxfrd  4651  ralxfr2d  4653  orduniorsuc  4724  ordzsl  4739  tfinds  4753  elres  5093  sotri3  5176  2elresin  5460  f1ocnv  5591  tz6.12c  5654  fveqres  5667  fvun1  5697  dffo4  5787  fconst5  5849  fnpr  5850  fnprOLD  5851  isores3  5955  f1owe  5973  f1oweALT  5974  weniso  5975  ndmovordi  6138  fnse  6360  tposfo2  6399  issmo2  6508  iordsmo  6516  smoel2  6522  tz7.48lem  6595  abianfp  6613  oawordeulem  6694  om00  6715  omlimcl  6718  odi  6719  nnawordi  6761  fiint  7280  fipreima  7308  dffi2  7323  suplub2  7359  wemapso2lem  7412  unwdomg  7445  inf3lem3  7478  trcl  7557  fidomtri  7773  prdom2  7783  cardaleph  7863  ackbij1lem16  8008  coflim  8034  coftr  8046  infpssrlem4  8079  isfin7-2  8169  axdc3lem2  8224  axdc3lem4  8226  brdom6disj  8304  entric  8326  fpwwe2lem12  8410  inatsk  8547  grur1a  8588  indpi  8678  reclem3pr  8820  supsrlem  8880  lelttr  9059  fimaxre  9848  nnmulcl  9916  arch  10111  nnnegz  10178  zeo  10248  uzm1  10409  negn0  10455  rpneg  10534  xrlttri  10625  xrlelttr  10639  iccid  10854  icoshft  10911  fzen  10964  elfz2nn0  10974  fzm1  11017  hasheqf1oi  11522  hashnfinnn0  11530  max0add  12002  abslt  12005  absle  12006  rexuzre  12043  caurcvg  12357  caucvg  12359  dvdsval2  12742  negdvdsb  12753  muldvds2  12762  smuval2  12881  smupvallem  12882  rplpwr  12943  alginv  12953  algfx  12958  rpexp1i  13008  qnumdencl  13018  phiprmpw  13052  prmdiveq  13062  pcmpt  13148  infpnlem1  13165  imasaddfnlem  13640  plelttr  14316  lubid  14326  mndodconglem  15066  cnpnei  17210  uncon  17372  kqsat  17639  isr0  17645  qtophmeo  17725  trufil  17818  alexsubALT  17958  bl2in  18170  addcnlem  18582  rescncf  18615  ovoliunlem2  19077  voliun  19126  mbflimsup  19236  itgcn  19412  dvdsq1p  19761  aalioulem2  19928  recosf1o  20115  logrec  20339  xrlimcnp  20485  basellem4  20544  bposlem1  20746  bposlem5  20750  lgsdchrval  20809  pntlem3  20981  usgraedgprv  21074  usgraedgrnv  21075  usgrafisinds  21097  eupai  21201  elghomlem2  21461  blocn2  21820  htthlem  21931  axhcompl-zf  22012  spanuni  22557  spansncol  22581  spansneleq  22583  elspansn5  22587  idcnop  22995  pjnormssi  23182  dmdmd  23314  bian1d  23463  eqrd  23511  ifeqeqx  23520  rnmpt2ss  23610  supxrnemnf  23648  iocinif  23666  rexdiv  23696  unitdivcld  23775  cnre2csqlem  23784  tpr2rico  23786  lmxrge0  23813  cnextcn  23824  ucnima  23896  iducn  23898  qqhval2lem  23958  esumpr2  24044  esumcvg  24062  issgon  24092  measxun2  24148  measres  24160  measdivcstOLD  24162  measdivcst  24163  imambfm  24196  cnmbfm  24197  mbfmco2  24199  elorrvc  24290  erdsze2lem2  24459  cvmsval  24521  ghomgsg  24672  ghomf1olem  24673  dedekindle  24757  gammadmaddnn0  24914  fundmpss  24948  dfon2lem3  24967  frmin  25068  poseq  25079  soseq  25080  wfrlem5  25086  wfrlem10  25091  wfrlem12  25093  frrlem5  25111  frrlem11  25119  nobndup  25180  nobnddown  25181  dfrdg4  25315  brbtwn2  25360  axbtwnid  25394  cgrtriv  25452  btwntriv2  25462  ifscgr  25494  lineext  25526  btwnconn1lem12  25548  colinbtwnle  25568  ontgval  25697  onsucconi  25703  ltflcei  25753  itg2addnclem  25760  areacirclem4  25787  areacirclem6  25790  areacirc  25791  elicc3  25820  comppfsc  25899  nninfnub  26053  prdstotbnd  26109  heiborlem4  26129  heibor  26136  grpokerinj  26166  isidlc  26231  prtlem17  26335  elrfirn2  26362  rencldnfilem  26494  sdrgacs  27100  stoweidlem18  27358  stoweidlem27  27367  stoweidlem35  27375  stoweidlem48  27388  rexrsb  27538  funbrafv  27614  rlimdmafv  27633  snelpwrVD  28358  en3lplem1VD  28371  en3lpVD  28373  orbi1rVD  28376  sbc3orgVD  28379  3impexpVD  28384  equncomVD  28396  trsbcVD  28405  trintALTVD  28408  trintALT  28409  csbingVD  28412  csbsngVD  28421  csbxpgVD  28422  csbrngVD  28424  csbfv12gALTVD  28427  relopabVD  28429  e2ebindVD  28440  bnj580  28697  ax10lem4NEW7  28884  dral1NEW7  28906  cbvalwwAUX7  28930  ax16iNEW7  28962  sbequiNEW7  28989  speivNEW7  29033  ax7w6AUX7  29059  cbvalOLD7  29116  a16gALTOLD7  29135  sb9iOLD7  29149  ax10lem18ALT  29183  lsator0sp  29250  atlrelat1  29570  cvratlem  29669  diaintclN  31307  dibintclN  31416  cdlemn11pre  31459  dihord2pre  31474  dihintcl  31593  dochkrshp4  31638  lcfrlem9  31799  lcfrlem21  31812  mapdh8e  32033
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