Theorem biimp 151

Description: Infer an implication from a logical equivalence.

Hypothesis

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

Assertion

Ref	Expression
biimp	|- (ph -> ps)

Proof of Theorem biimp

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

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

This theorem is referenced by:  bicomi 172  bitr 173  imbi2i 185  imbi1i 186  negbii 187  mpbi 189  sylib 198  sylbi 199  syl5ib 206  syl6ib 212  syl7ib 216  syl8ib 217  con1bii 220  pm1.2 245  pm1.4 247  pm2.62 248  orel1 251  pm1.5 259  pm2.32 262  pm3.1 314  pm3.26bi 322  pm3.27bi 326  pm3.3 348  pm3.22 441  sylanb 452  sylan2b 455  anbi2i 483  dfbi 518  pm5.16 670  nbn2 725  bimsc1 754  syl3an1b 866  syl3an2b 867  syl3an3b 868  nicodraw 956  mpgbiOLD 992  stdpc5 1064  19.25 1090  sbbii 1180  exmoeu 1419  2mo 1454  eqeq1 1488  eleq2 1542  moeq 1927  ssel 2072  ss0 2313  prprc 2466  snsspr 2482  eqsn 2486  elinti 2554  trel 2700  moabex 2780  pocl 2858  unexg 2888  unisn2 2889  reuunixfr 2920  wefrc 2957  ordsson 3005  dflim3 3132  peano2 3164  elrel 3267  dmsnop 3342  dmxp 3346  coi2 3525  nfunv 3560  funun 3568  funcnv3 3572  funimass1 3586  funssxp 3652  f1o2 3707  f1ocnv 3715  f1o00 3728  elrnopabg 3814  fsn2 3850  tz7.49c 3974  1stval 4095  2ndval 4096  1st2val 4109  2nd2val 4110  1stdm 4123  oaabs 4266  elqsi 4305  qsexg 4308  0nelqs 4312  bren2 4403  pw2en 4461  canth2 4499  limenpsi 4520  php4 4531  unfilem1 4561  abfii4 4574  supmaxlem 4598  preleq 4615  inf3lem2 4626  r1tr 4666  rankr1 4686  rankr1b 4711  rankxplim2 4725  ac6lem 4766  kmlem6 4782  fodom 4810  unidom 4820  isinfcard 4900  iscard3 4901  alephval3 4916  dominf 4917  xrrebndt 5581  add20 5615  posex 5914  supxrun 6091  dfn2 6118  elnn0nn 6177  icoshftf1oi 6359  seq1lem2 6493  expnlbndt 6668  nn0opthlem2 6679  cru 6751  recvalz 6901  binomlem1 7080  binomlem2 7081  isumnul 7217  geoser 7248  ivthlem6 7300  ivthlem7 7301  efaddlem5 7356  efsubt 7385  eirrlem5 7407  abspef01tlub 7409  efgt1 7417  reeff1olem1 7438  sin01bndlem2 7483  sin01bndlem3 7484  cos01bndlem2 7485  cos01bndlem3 7486  sin01gt0 7491  cos01gt0 7492  sin02gt0 7493  ruclem24 7548  ruclem27 7551  ruclem28 7552  infxpidmlem8 7574  isbasis3g 7625  sn0top 7657  isopn2 7682  ntrval2 7695  innei 7745  cnpco 7778  dfms2 7808  metssba2 7819  grpidinvlem3 8059  issubg 8124  subgres 8125  subgid 8128  subgabl 8131  sspval 8390  nmlno0lem 8461  blocni 8473  pythi 8518  pilem2 8679  pilem3 8680  efif 8728  efifolem7 8735  efif1lem3 8739  efif1lem4 8740  circgrp 8747  effoi 8752  normpyth 9016  omlsilem 9251  pjch 9272  shmods 9369  chlubi 9402  nmlnop0ALT 9927  nmopunt 9946  nmcopexlem1 9958  nmcfnexlem1 9987  cnlnssadj 10020  nmopco 10035  mdbr3 10232  mdbr4 10233  ssmd1 10246  dmdsl3t 10250  mdslmd1lem2 10261  mdslmd4 10268  mdexch 10270  atssmat 10313  atoml2 10318  irredlem3 10327  mdsymlem1 10338  mdsymlem3 10340  dmdbr6at 10358  dmdbr7at 10359  cdjreu 10367  ghomgrpilem2 10394  faimpex 10446  difeqri2 10451  infi1 10454  fine 10455  ficli 10475  mapdiscn 10517  cmphmp 10527  cnvhmphb 10532  cnvhmph 10533  hmphsyma 10534  hmeobc 10548  filintf 10574  fgsb 10575  efilcp 10576  infi 10579  efilcp2 10581  cnfilca 10582  rcfpfillem4 10586  sfvlim 10596  sfvlimOLD 10597  dtopcl 10606  dtt2 10609  isalg 10644  algi 10651  homib 10715  cmpmon 10734  idmon 10736  iepiclem 10742

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 147

Copyright terms: Public domain