Theorem biimpri 168

Description: Infer a converse implication from a logical equivalence.

Hypothesis

Ref	Expression
biimpr.1	|- (ph <-> ps)

Assertion

Ref	Expression
biimpri	|- (ps -> ph)

Proof of Theorem biimpri

Step	Hyp	Ref	Expression
1		biimpr.1	. 2 |- (ph <-> ps)
2		bi2 165	. 2 |- ((ph <-> ps) -> (ps -> ph))
3	1, 2	ax-mp 7	1 |- (ps -> ph)

Syntax hints:   -> wi 3   <-> wb 162

This theorem is referenced by:  bicomi 188  bitri 189  imbi2i 201  imbi1i 202  notbii 203  mpbir 206  sylibr 216  sylbir 217  syl5ibr 223  syl6ibr 229  con1bii 236  pm2.54 243  pm2.68 268  pm2.31 280  pm3.2 303  pm3.11 340  pm3.31 374  pm3.26bi2 464  pm3.44 474  sylanbr 497  sylan2br 500  anbi2i 535  dfbi 570  pm3.43 661  pm5.15 726  rnlem 850  syl3an1br 983  syl3an2br 984  syl3an3br 985  nic-axALT 1087  3ornot23 1123  3impexpbicom 1129  sbbii 1376  a12lem1 1605  mo2 1633  exmoeu 1646  2euexOLD 1682  2mo 1688  eueq2 2262  eueq3 2263  ssunieq 3033  intab 3069  frirr 3449  ordunidif 3527  sucidOLD 3559  unizlim 3597  dfwe2 3672  tfindsOLD 3754  nnsuc 3780  opresOLD 4037  ndmima 4111  dffn2OLD 4375  dffo2 4432  dff1o2 4450  dff1o2OLD 4451  resdif 4470  f1o00 4479  fvimacnvALT 4593  exfo 4606  fopabco 4616  f1stres 4845  f2ndres 4846  1st2val 4849  2nd2val 4850  iotabi 4905  uniabio 4906  tz7.44-3 4949  tz7.49 4979  abianfp 4982  unblem4 5446  ordiso 5493  inf3lem3 5530  trcl 5561  en3lplem2 5566  kmlem1 5723  brdom3 5759  brdom5 5760  brdom4 5761  brdom6disj 5763  ficardom 5775  ondomcard 5805  ltexpq 6028  suppsr3 6172  axcnre 6235  ssxr 6510  le2tri3i 6560  0nn0 7117  elnnnn0b 7177  elnnnn0c 7178  uzind4 7414  sqr2irrlem1 7769  absdivzi 7905  abs1mi 7951  seq1ubi 7959  binomlem5 8125  iserzexi 8201  ivthlem2 8339  ivthlem7 8344  ivthlem8 8345  ef01tlubi 8443  absef01tlubi 8445  efcnlem1 8479  sincos1sgn 8540  sincos2sgn 8541  znnen 8566  tgcl 8689  sn0top 8712  elcls 8775  cnpfval 8828  cnpnei 8838  cnconst 8852  blval 8909  bl2in 8915  bcthlem17 9088  grplactf1o 9201  issubgi 9226  subgabl 9227  ghgrpi 9240  vacnlem3 9464  sm1cnilem 9481  blo3i 9597  pilem1 9815  pilem3 9817  sinhalfpilem 9823  sincos4thpi 9855  cosh111 9866  efif 9870  efifolem1 9871  efifolem2 9872  efifolem3 9873  efifolem5 9875  efifolem6 9876  efif1lem6 9884  efielcirc 9888  effoi 9894  resslogrn 9902  pilog 9917  oprabco 9953  fiv 10005  tx1cn 10015  tx2cn 10016  2txcn 10021  subtopmet 10048  filintf 10066  oefil2 10067  sfvlim 10088  ismnd2 10184  unmnd 10197  zrdivrng 10210  hhsscms 10575  hsupval2 10725  cmcmlem 10959  lnopconi 11392  lnfnconi 11419  cnvbraval 11473  leopnmid 11501  csmdsymi 11698  irredlem4 11757  sumdmdlem 11782  bnj134 12270  bnj1136 13227  bnj1152 13229  bnj1175 13235  bnj1408 13316  bnj1450 13333  fz1eqblem 13400  ghomfo 13426  ghomf1olem 13429  divalglem7 13494  ndvdsadd 13503  gcdcllem1 13510  gcdcllem3 13512  mulgcdlem2 13549  mulgcdlem7 13554  1idssfct 13562  zgt1b1 13563  2prm 13571  3prm 13572  elres 13618  dfon2lem3 13642  dfon2lem7 13646  dfon2lem9 13648  sspred 13677  soxp 13742  frxp 13743  sltval2 13789  axdenselem5 13813  nabi1 13869  nabi2 13870  df3nandALT1 13876  lukshef-ax2 13969  arg-ax 13970  nandsym1 13976  bibox 14037  binxt 14039  evpexun 14050  difeqri2 14069  cpref 14102  fldleqt 14115  twsymr 14124  celsor 14173  prjnpl 14236  dstr 14242  inposet 14344  dfps2 14359  svs2 14552  fisub 14638  clindistop 14676  topsinind 14681  idtrgrp 14692  invtrgrp 14693  isalg 14750  intartar 14937  elfiun 15051  ordisoOLD 15056  opnnei 15099  reconnlem1 15128  locfincomp 15196  locfincf 15198  comppfsc 15199  topmeet 15208  topjoin 15209  fixufil 15258  ufinffr 15260  fclsfnflim 15296  filnetlem1 15322  filnetlem5 15326  euuni2 15345  difxp 15372  fnopabco 15393  fipreima 15438  inficl 15439  zornn0 15446  frfi 15453  sdclem1 15491  sdclem2 15492  seq1eq2 15499  geomcau 15531  sstotbnd 15618  totbndss 15619  heiborlem8 15644  heiborlem10 15646  heiborlem14 15650  heiborlem19 15655  heiborlem26 15662  heiborlem29 15665  heiborlem37 15673  heiborlem38 15674  heiborlem41 15677  phtpycolem4 15736  phtpcer 15744  pcocn 15758  pcohtpy 15765  pcoass 15767  pi1gp 15777  isfld2 15835  igenval2 15896  isfldidl 15898  dmncan2 15907  prtlem10 15947  dfvd1impr 16145  dfvd2impr 16163  e1bir 16178  e2bir 16181  e3bir 16268  19.21a3con13vVD 16335  3impexpbicomVD 16340  tratrbVD 16344  strbi 16471  lubprop 16563  glbprop 16568  atombase 16752

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 163

Copyright terms: Public domain