Theorem biimp 133

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 130	. 2 |- ((ph <-> ps) -> (ph -> ps))
3	1, 2	ax-mp 6	1 |- (ph -> ps)

Syntax hints:   -> wi 2   <-> wb 127

This theorem is referenced by:  bicomi 150  bitr 151  imbi2i 160  imbi1i 161  negbii 162  mpbi 164  sylib 173  sylbi 174  syl5ib 181  syl6ib 185  bisyl7 189  bisyl8 190  bicon1i 193  pm2.62 210  orel1 212  pm3.26bd 259  pm3.27bd 263  sylanb 344  sylan2b 347  anbi2i 367  bimsc1 557  syl3an1b 622  syl3an2b 623  syl3an3b 624  mpgbi 685  stdpc5 739  19.25 763  bisb 855  exmoeu 1039  eupickb 1056  cleq1 1107  eleq2 1150  moeq 1431  ssel 1502  ss0 1727  snsspr 1853  moabex 1868  elinti 1974  iunpw 2040  trel 2048  pocl 2132  wefrc 2195  ordsson 2242  limsuclem 2360  dflim3 2368  peano2 2391  dmsnop 2547  dmxp 2552  coi2 2666  nfunv 2693  funun 2700  funimass1 2712  f1o2 2804  f1ocnv 2811  f1o00 2823  fsn2 2896  tz7.49c 2998  1stval 3089  2ndval 3090  1st2val 3097  elqsi 3228  0nelqs 3234  bren2 3293  pw2en 3348  canth2 3381  mapdom2lem 3388  limenpsi 3400  php4 3412  unfilem1 3438  preleq 3454  inf3lem2 3465  r1tr 3498  rankr1 3518  ac6lem 3575  kmlem6 3585  fodom 3613  isinfcard 3692  iscard3 3693  alephprc 3698  divdivdivt 4265  add20 4329  posex 4422  cru 4529  nn0ge0i 4559  elnn0nn 4593  seqlem2 4663  nn0opthlem2 4723  ruclem8 4892  ruclem24 4908  ruclem27 4911  ruclem28 4912  infxpidmlem8 4940  normpyth 5090  omlsilem 5249  pjch 5269  shmods 5363  chlubi 5393  mdbr3 5729  mdbr4 5730  ssmd1 5734  mdsymlem1 5776  mdsymlem3 5778

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

This theorem depends on definitions:  df-bi 128

metamath.org