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 440  sylanb 451  sylan2b 454  anbi2i 482  dfbi 517  pm5.16 669  nbn2 723  bimsc1 752  syl3an1b 864  syl3an2b 865  syl3an3b 866  nicodraw 954  mpgbi 989  stdpc5 1060  19.25 1086  sbbii 1176  exmoeu 1415  2mo 1450  eqeq1 1484  eleq2 1538  moeq 1923  ssel 2067  ss0 2308  prprc 2459  snsspr 2475  eqsn 2479  elinti 2547  trel 2693  moabex 2773  pocl 2851  unexg 2881  unisn2 2882  reuunixfr 2913  wefrc 2950  ordsson 2998  dflim3 3125  peano2 3157  elrel 3260  dmsnop 3335  dmxp 3339  coi2 3518  nfunv 3553  funun 3561  funcnv3 3565  funimass1 3579  funssxp 3645  f1o2 3700  f1ocnv 3708  f1o00 3721  elrnopabg 3807  fsn2 3843  tz7.49c 3967  1stval 4088  2ndval 4089  1st2val 4102  2nd2val 4103  1stdm 4116  oaabs 4259  elqsi 4298  qsexg 4301  0nelqs 4305  bren2 4396  pw2en 4453  canth2 4491  limenpsi 4512  php4 4524  unfilem1 4562  supmaxlem 4604  preleq 4619  inf3lem2 4630  r1tr 4671  rankr1 4691  rankr1b 4716  rankxplim2 4730  ac6lem 4771  kmlem6 4787  fodom 4815  unidom 4825  isinfcard 4905  iscard3 4906  alephval3 4921  dominf 4922  dominfOLD 4923  xrrebndt 5587  add20 5621  posex 5917  supxrun 6094  dfn2 6121  elnn0nn 6180  seq1lem2 6318  icoshftf1oi 6417  expnlbndt 6663  nn0opthlem2 6673  cru 6745  recvalz 6894  binomlem1 7073  binomlem2 7074  isumnul 7210  geoser 7241  ivthlem6 7293  ivthlem7 7294  efaddlem5 7349  efsubt 7378  eirrlem5 7400  abspef01tlub 7402  efgt1 7410  reeff1olem1 7431  sin01bndlem2 7476  sin01bndlem3 7477  cos01bndlem2 7478  cos01bndlem3 7479  sin01gt0 7484  cos01gt0 7485  sin02gt0 7486  ruclem24 7541  ruclem27 7544  ruclem28 7545  infxpidmlem8 7567  isbasis3g 7619  sn0top 7651  isopn2 7677  ntrval2 7690  innei 7740  cnpco 7773  dfms2 7803  metssba2 7814  grpidinvlem3 8054  issubg 8119  subgres 8120  subgid 8123  subgabl 8126  sspval 8385  nmlno0lem 8456  blocni 8468  pythi 8513  pilem2 8674  pilem3 8675  efif 8723  efifolem7 8730  efif1lem3 8734  efif1lem4 8735  circgrp 8742  effoi 8747  normpyth 9011  omlsilem 9246  pjch 9267  shmods 9364  chlubi 9397  nmlnop0ALT 9922  nmopunt 9941  nmcopexlem1 9953  nmcfnexlem1 9982  cnlnssadj 10015  nmopco 10030  mdbr3 10227  mdbr4 10228  ssmd1 10241  dmdsl3t 10245  mdslmd1lem2 10256  mdslmd4 10263  mdexch 10265  atssmat 10308  atoml2 10313  irredlem3 10322  mdsymlem1 10333  mdsymlem3 10335  dmdbr6at 10353  dmdbr7at 10354  cdjreu 10362  ghomgrpilem2 10389  faimpex 10441  difeqri2 10446  infi1 10449  fine 10450  ficli 10470  mapdiscn 10505  cmphmp 10515  cnvhmphb 10520  cnvhmph 10521  hmphsyma 10522  hmeobc 10536  filintf 10562  fgsb 10563  efilcp 10564  infi 10567  efilcp2 10569  cnfilca 10570  rcfpfillem4 10574  sfvlim 10584  sfvlimOLD 10585  dtopcl 10594  dtt2 10597  isalg 10632  algi 10639  homib 10703  cmpmon 10722  idmon 10724

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