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 438  sylanb 449  sylan2b 452  anbi2i 480  pm5.16 666  nbn2 720  bimsc1 749  syl3an1b 861  syl3an2b 862  syl3an3b 863  nicodraw 950  mpgbi 985  stdpc5 1056  19.25 1082  sbbii 1172  exmoeu 1411  2mo 1445  eqeq1 1478  eleq2 1532  moeq 1916  ssel 2059  ss0 2299  prprc 2450  snsspr 2466  eqsn 2470  elinti 2537  trel 2682  moabex 2761  pocl 2839  unexg 2869  unisn2 2870  reuunixfr 2901  wefrc 2938  ordsson 2986  dflim3 3113  peano2 3145  elrel 3248  dmsnop 3323  dmxp 3327  coi2 3503  nfunv 3538  funun 3546  funcnv3 3550  funimass1 3564  funssxp 3629  f1o2 3684  f1ocnv 3692  f1o00 3705  elrnopabg 3791  fsn2 3827  tz7.49c 3951  1stval 4071  2ndval 4072  1st2val 4085  2nd2val 4086  1stdm 4099  oaabs 4242  elqsi 4281  qsexg 4284  0nelqs 4288  bren2 4376  pw2en 4432  canth2 4470  limenpsi 4491  php4 4502  unfilem1 4530  abfii4 4544  supmaxlem 4568  preleq 4583  inf3lem2 4594  r1tr 4634  rankr1 4654  rankr1b 4679  rankxplim2 4693  ac6lem 4734  kmlem6 4750  fodom 4778  unidom 4788  isinfcard 4867  iscard3 4868  alephval3 4883  dominf 4884  xrrebndt 5549  add20 5584  posex 5864  supxrun 6040  dfn2 6067  elnn0nn 6126  seq1lem2 6255  icoshftf1oi 6350  nn0opthlem2 6603  cru 6675  recvalz 6833  binomlem1 7012  binomlem2 7013  isumnul 7146  geoser 7177  ivthlem6 7229  ivthlem7 7230  ivthlem4OLD 7236  ivthlem6OLD 7238  ivthlem7OLD 7239  ivthOLD 7241  ivth2OLD 7242  efaddlem5 7292  efsubt 7321  eirrlem5 7342  abspef01tlub 7344  efgt1 7352  reeff1olem1 7372  reeff1olem1OLD 7374  sin01bndlem2 7418  sin01bndlem3 7419  cos01bndlem2 7420  cos01bndlem3 7421  sin01gt0 7426  cos01gt0 7427  sin02gt0 7428  ruclem24 7484  ruclem27 7487  ruclem28 7488  infxpidmlem8 7510  isbasis3g 7563  subbas 7594  sn0top 7597  isopn2 7623  ntrval2 7636  innei 7686  cnpco 7719  dfms2 7749  metssba2 7760  grpidinvlem3 8000  issubg 8068  subgres 8069  subgid 8072  subgabl 8075  sspval 8329  nmlno0lem 8398  blocni 8409  pythi 8454  pilem2 8610  pilem3 8611  efif 8655  efifolem4 8659  efifolem7 8662  efif1lem3 8666  efif1lem4 8667  circcltOLD 8675  circgrp 8679  effoi 8684  normpyth 8948  omlsilem 9182  pjch 9203  shmods 9300  chlubi 9333  nmlnop0ALT 9858  nmopunt 9877  nmcopexlem1 9889  nmcfnexlem1 9918  cnlnssadj 9951  nmopco 9966  mdbr3 10162  mdbr4 10163  ssmd1 10175  dmdsl3t 10179  mdslmd1lem2 10190  mdslmd4 10197  mdexch 10199  atssmat 10242  atoml2 10247  irredlem3 10256  mdsymlem1 10267  mdsymlem3 10269  dmdbr6at 10285  cdjreu 10293  ghomgrpilem2 10320  gelcomplOLD 10353  faimpex 10375  difeqri2 10380  infi1 10383  fine 10384  ficli 10404  mapdiscn 10434  cmphmp 10444  cnvhmphb 10449  cnvhmph 10450  hmphsyma 10451  filintf 10479  fgsb 10480  efilcp 10481  infi 10484  efilcp2 10486  cnfilca 10487  dtopcl 10495  dtt2 10498  isalg 10533  algi 10540  homib 10604  cmpmon 10621  idmon 10624

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