Theorem biimpi 167

Description: Infer an implication from a logical equivalence.

Hypothesis

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

Assertion

Ref	Expression
biimpi	|- (ph -> ps)

Proof of Theorem biimpi

Step	Hyp	Ref	Expression
1		biimp.1	. 2 |- (ph <-> ps)
2		bi1 164	. 2 |- ((ph <-> ps) -> (ph -> ps))
3	1, 2	ax-mp 7	1 |- (ph -> ps)

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

This theorem is referenced by:  bicomi 188  bitri 189  imbi2i 201  imbi1i 202  notbii 203  mpbi 205  sylib 214  sylbi 215  syl5ib 222  syl6ib 228  syl7ib 232  syl8ib 233  con1bii 236  pm1.2 263  pm1.4 265  pm2.62 266  orel1 269  pm1.5 277  pm2.32 281  pm3.1 339  pm3.26bi 347  pm3.27bi 351  pm3.3 373  pm3.22 484  sylanb 496  sylan2b 499  anbi2i 535  dfbi 570  pm5.16 727  nbn2 787  bimsc1 820  rnlem 850  3simp1bi 887  3simp2bi 888  3simp3bi 889  syl3an1b 980  syl3an2b 981  syl3an3b 982  nic-ax 1086  3ornot23 1123  stdpc5 1243  19.25 1273  sbbii 1376  exmoeu 1646  2mo 1688  eqeq1 1727  eleq2 1795  gencbvex 2167  moeq 2264  euind 2272  reuind 2283  ssel 2448  n0moeu 2712  ss0 2727  prprc 2932  snsspr1OLD 2958  eqsn 2965  elintiOLD 3046  trelOLD 3237  snex 3307  unipw 3319  moabex 3328  pocl 3411  wefrc 3467  unexg 3609  unisn2 3610  reuunixfr 3661  ordsson 3678  ordssonOLD 3679  dflim3OLD 3742  peano2 3783  elrel 3897  dmxp 3988  dmxpOLD 3989  elimasni 4103  dmsnopOLD 4179  coi2 4225  nfunv 4264  funun 4273  funcnv3 4287  funimass1 4302  funssxp 4388  dff1o2OLD 4451  f1ocnvOLD 4463  f1o00 4479  nfunsnOLD 4518  dffv2 4545  elrnopabg 4584  fsn2 4620  1stval 4833  2ndval 4834  1stdm 4860  tz7.49c 4980  oaabs 5120  elqsi 5160  qsexg 5163  0nelqs 5168  bren2 5259  pw2en 5316  ac6sfi 5320  canth2 5359  riotaxfrd 5391  limenpsi 5409  php4 5420  unfilem1 5451  abfii4 5464  supmaxlem 5488  preleq 5518  inf3lem2 5529  en3lplem2 5566  r1tr 5574  rankr1 5594  rankr1b 5619  rankxplim2 5633  ac6lem 5712  kmlem6 5728  fodom 5756  unidom 5766  ficardom 5775  isinfcard 5831  iscard3 5832  alephval3 5847  dominf 5848  addcani 6301  xrrebnd 6539  add20i 6578  posexi 6886  supxrun 7089  dfn2 7116  elnn0nn 7175  zindd 7222  cardfz 7514  seq1lem2 7518  expnlbnd 7697  crui 7782  recvalzi 7934  binomlem1 8121  binomlem2 8122  isumnul 8259  geoseri 8291  efaddlem5 8399  eirrlem5 8450  efgt1i 8463  ruclem24 8597  ruclem27 8600  ruclem28 8601  infxpidmlem8 8623  isbasis3g 8677  subbas 8709  sn0top 8712  isopn2 8744  ntrval2 8757  innei 8807  cnpco 8841  dfms2 8871  metssba2 8882  grpidinvlem3 9125  gxsuc 9190  issubg 9220  gapmlem 9256  vacnlem3 9464  vacnlem6 9467  sspval 9516  nmlno0lem 9588  blocni 9600  pythi 9646  twpar2 9942  dif1enOLD 9967  dif1card 9969  fine 10006  txcn 10019  hmeobc 10031  subcld 10046  subtopmet 10048  filintf 10066  infi 10072  fbunfip 10074  sfvlim 10088  limfil 10089  hausfillim 10095  exidu1 10165  on1el3 10204  normpythi 10434  omlsilem 10669  pjchi 10690  shmodsi 10787  chlubii 10820  nmlnop0iALT 11349  nmopun 11368  nmcopexlem1 11380  nmcfnexlem1 11409  cnlnssadj 11442  nmopcoi 11457  mdbr3 11661  mdbr4 11662  ssmd1 11675  dmdsl3 11679  mdslmd1lem2 11690  mdslmd4i 11697  mdexchi 11699  atssma 11742  atoml2i 11747  irredlem3 11756  mdsymlem1 11767  mdsymlem3 11769  dmdbr6ati 11787  dmdbr7ati 11788  cdjreui 11796  addltmulALT 11810  bnj112 12249  bnj529 12327  bnj637 12364  bnj638 12365  bnj639 12366  bnj640 12367  bnj641 12368  bnj682 12409  bnj683 12410  bnj684 12411  bnj685 12412  bnj686 12413  bnj687 12414  bnj688 12415  bnj689 12416  bnj690 12417  bnj691 12418  bnj692 12419  bnj693 12420  bnj694 12421  bnj695 12422  bnj696 12423  bnj697 12424  bnj698 12425  bnj699 12426  bnj700 12427  bnj701 12428  bnj702 12429  bnj703 12430  bnj704 12431  bnj927 12627  bnj1150 12737  bnj1164 12748  bnj1191 12760  bnj1195 12768  bnj1215 12783  bnj1295 12833  bnj1343 12859  bnj1379 12892  bnj1424 12911  bnj1436 12922  bnj1471 12942  bnj1476 12948  bnj149 13033  bnj594 13092  bnj580 13093  bnj607 13096  bnj908 13121  bnj1066 13190  bnj1097 13204  bnj1118 13212  bnj1128 13220  bnj1125 13222  bnj1145 13223  bnj1152 13229  bnj1154 13230  bnj1172 13232  bnj1268 13264  bnj1388 13306  bnj1398 13307  bnj1417 13322  fz1eqblem 13400  ghomgrpilem2 13421  prmnn 13570  truni 13584  trint 13586  elres 13618  dfon2lem3 13642  dfon2lem7 13646  dfon2lem8 13647  predbr 13687  tz6.26 13705  poxp 13741  wfrlem4 13752  wfrlem5 13753  wfrlem10 13758  wfrlem15 13763  nabi1 13869  nabi2 13870  df3nandALT1 13876  lukshef-ax2 13969  nandsym1 13976  bibox 14037  binxt 14039  infi1 14071  ficli 14081  fldleqt 14115  twsymr 14124  imfstnrelc 14126  fldrels 14178  surjsec2 14196  fopab2g 14212  npincppr 14227  unprj 14237  domrancur1b 14274  supdef 14326  mxlmnl2 14334  supaub 14339  geme2 14341  defge2 14362  tostos 14363  toplat 14364  dfdir2 14365  clfsebsr 14432  gaplc 14454  rngapm 14456  fnopabco2b 14457  curgrpact 14458  muldisc 14547  svli2 14549  mapdiscnlem 14591  cmphmp 14598  cnvhmphb 14600  cnvhmph 14601  hmphsyma 14602  topgele 14629  fgsb 14635  efilcp 14636  efilcp2 14640  cnfilca 14641  rcfpfillem4 14645  dtopcl 14662  dtt2 14665  stfincomp 14673  trhom 14697  bsi2 14702  cntrsetlem 14709  flimfneic 14732  isalg 14750  algi 14756  dmrngcmp 14780  dualded 14814  dualcat2 14815  homib 14827  cmpmon 14846  idmon 14848  iepiclem 14854  idsubc 14881  idsubidsup 14887  idsubfun 14888  tarax3d2 14907  emptar 14913  intartar 14937  valdom 14943  inttaror 14959  trer 15043  finminlem 15049  clsun 15095  opnregcld 15097  cldregopn 15098  subsubtop 15105  cnsubsp 15108  cnsubsp2 15109  compsublem 15112  compsub 15113  compfipin0 15118  alexsublem4 15122  dfcon2 15124  connsub 15125  reconnlem1 15128  reconn 15133  ivthALT 15136  2ndcsb 15158  2ndcctbss 15160  ssref 15174  topfneec 15183  fnessref 15185  refssfne 15186  locfindsc 15197  comppfsc 15199  topmtcl 15207  fnejoin1 15212  fnejoin2 15213  isnrm2 15234  opnfbas 15239  supfil 15242  isufil2 15247  ufprim 15251  ufileu 15255  filufint 15256  ufinffr 15260  sfcls 15286  filclus 15287  fclsfnflim 15296  flimfnfcls 15297  f1ocan2fv 15400  eropreu 15415  findcard2 15427  fimax 15428  indexfi 15437  frinfm 15440  welb 15441  nninfnub 15501  subspopn 15519  subspcld 15520  subspabs 15522  mettrifi 15529  caushft 15533  cnres 15571  paste 15575  sstotbnd 15618  bndss 15624  totbndbnd 15626  heiborlem26 15662  heiborlem37 15673  heiborlem42 15678  bfp 15691  rrnmet 15698  rrndstprj1 15699  rrndstprj2 15700  rrncms 15701  rrntotbnd 15704  phtpycom 15732  phtpcer 15744  pcohtpylem2 15763  ispridl2 15868  ersym2 15938  ertr2 15939  prtlem10 15947  pm10.12 15986  pm11.58 16029  pm11.61 16032  ax10-16 16047  pm13.192 16056  sbiota1 16081  dfvd1imp 16144  dfvd2imp 16162  e1bi 16177  e2bi 16180  e3bi 16267  3ornot23VD 16330  3impexpbicomVD 16340  3impexpbicomiVD 16341  tratrbVD 16344  strbi 16471  ps-1 16807  grpidinvlem3NEW 16840  pluspssat 16988

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