Theorem biimpi 120

Description: Infer an implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.)

Hypothesis

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

Assertion

Ref	Expression
biimpi	|- ( ph -> ps )

Proof of Theorem biimpi

Step	Hyp	Ref	Expression
1		biimpi.1	. 2 |- ( ph <-> ps )
2		biimp 118	. 2 |- ( ( ph <-> ps ) -> ( ph -> ps ) )
3	1, 2	ax-mp 5	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylbi  121  sylib  122  sylbb  123  biimpri  133  mpbi  145  biimtrid  152  imbitrdi  161  syl7bi  165  syl8ib  166  bitri  184  simplbi  274  simprbi  275  sylanb  284  sylan2b  287  anc2l  327  birani  386  bilani  387  sylanblc  419  orbi2i  774  pm2.32  781  oranim  793  stabnot  845  exmiddc  848  pm2.1dc  849  stdcndcOLD  858  stdcn  859  const  864  imanst  900  pm5.75  975  rnlem  989  ifpnst  1001  simp1bi  1043  simp2bi  1044  simp3bi  1045  syl3an1b  1314  syl3an2b  1315  syl3an3b  1316  exalim  1555  nford  1620  nfal  1629  stdpc5  1637  sbbii  1818  sb9i  2040  eu5  2134  exmoeudc  2150  eqeq1  2245  eleq2  2302  nner  2424  rexalim  2543  gencbvex  2869  gencbval  2871  moeq  3001  euind  3013  reuind  3031  ssel  3242  ssrmof  3311  unssd  3405  ssind  3455  unssdif  3466  ss0  3563  rabsnif  3777  prprc  3821  disjnim  4118  trint  4242  snexprc  4321  undifexmid  4328  exmidn0m  4336  exmidsssn  4337  exmidundif  4341  exmidundifim  4342  exmid1stab  4343  pocl  4446  sotritrieq  4468  frirrg  4493  unexg  4587  abnex  4591  reusv3i  4603  ordtriexmid  4666  ontriexmidim  4667  ordtri2orexmid  4668  preleq  4700  0elsucexmid  4710  ordpwsucexmid  4715  ordtri2or2exmid  4716  elomssom  4750  brrelex12  4811  0nelrel  4819  elrel  4875  xpssres  5096  elres  5097  coi2  5302  iotabi  5345  uniabio  5346  nfunv  5408  funun  5420  funcnv3  5441  funimass1  5456  imain  5461  funssxp  5555  f0dom0  5584  f1o00  5674  fsn2  5876  funopsn  5885  isoselem  6019  oprabid  6110  brabvv  6127  uchoice  6364  oprssdmm  6398  1stdm  6409  f1o2ndf1  6457  poxp  6461  suppval1  6472  funsssuppss  6491  rdgon  6650  frecfcllem  6668  nntri3or  6759  nntri1  6762  ensym  7061  en2  7105  xpen  7138  snnen2oprc  7154  phplem4on  7162  fict  7163  fidceq  7164  infiexmid  7174  php5fin  7179  fisbth  7180  fin0  7182  fin0or  7183  diffisn  7190  infnfi  7192  fidcen  7196  en2eqpr  7207  exmidpw  7208  exmidpweq  7209  pw1fin  7210  fientri3  7215  unsnfi  7219  unsnfidcex  7220  unsnfidcel  7221  undifdcss  7223  ssfidc  7238  relcnvfi  7248  fiuni  7305  eqinfti  7353  djulclb  7388  updjud  7415  omp1eomlem  7427  0ct  7440  ctmlemr  7441  ctssdclemn0  7443  ctssdccl  7444  enomnilem  7471  finomni  7473  exmidomni  7475  enmkvlem  7494  enwomnilem  7502  exmidontriimlem1  7570  onntri35  7589  onntri52  7596  dftap2  7610  exmidapne  7619  enq0sym  7792  enq0tr  7794  prarloclem3  7857  nqprl  7911  nqpru  7912  addnqprlemrl  7917  addnqprlemru  7918  addnqprlemfl  7919  addnqprlemfu  7920  mulnqprlemrl  7933  mulnqprlemru  7934  mulnqprlemfl  7935  mulnqprlemfu  7936  ltexprlemfl  7969  ltexprlemfu  7971  recexprlemopl  7985  recexprlemopu  7987  aptipr  8001  cauappcvgprlemladdfu  8014  cauappcvgprlemladdfl  8015  caucvgprlemladdfu  8037  caucvgprprlemexbt  8066  suplocexprlemrl  8077  suplocexprlemru  8079  suplocexprlemex  8082  srpospr  8143  elrealeu  8189  axarch  8251  axcaucvglemres  8259  nn0ge2m1nn  9609  elnn0z  9639  peano2z  9662  uzm1  9935  qapne  10021  rpregt0  10050  rpnegap  10069  xnn0dcle  10186  xnn0letri  10187  npnflt  10199  nmnfgt  10202  xaddf  10228  xaddval  10229  xltadd1  10260  xsubge0  10265  xleaddadd  10271  elfz1end  10442  1fv  10527  elfzonlteqm1  10609  qtri3or  10656  exbtwnzlemshrink  10664  rebtwn2zlemshrink  10669  ioom  10676  elicore  10682  modfzo0difsn  10813  modsumfzodifsn  10814  addmodlteq  10816  frecfzennn  10844  seq3f1olemstep  10932  ser0  10951  exp3vallem  10958  facp1  11149  faclbnd  11160  bcn1  11177  hashennnuni  11199  hashcl  11201  hashfz1  11203  hashen  11204  fihashdom  11224  hashun  11226  zfz1isolem1  11273  zfz1iso  11274  lencl  11289  sswrd  11294  swrdswrd  11458  swrdccatin2  11482  pfxccat3  11487  pfxccatpfx1  11489  sqrt0  11751  resqrexlemfp1  11756  cau3lem  11861  xrmaxifle  11993  xrmaxiflemval  11997  xrmaxltsup  12005  xrmaxadd  12008  climserle  12092  climcaucn  12098  iserabs  12223  isumshft  12238  cvgratgt0  12281  mertenslem2  12284  prodf1  12290  fprodunsn  12352  fprodfac  12363  eirrap  12526  bezoutlemzz  12760  dfgcd3  12768  nnmindc  12792  nnminle  12793  nninfctlemfo  12798  lcmcllem  12826  prmind2  12879  prm2orodd  12885  sqrt2irr0  12923  sqrt2irrap  12939  ballotfilem2  13209  ballotfilemic  13231  ballotfilem1c  13232  ennnfonelemjn  13274  ennnfonelemdm  13292  ennnfonelemim  13296  ctiunctlemfo  13311  isstructr  13348  basmex  13393  dfgrp2  13812  dfgrp3mlem  13883  mulgnngzsum  13910  grpissubg  13977  ablsubsub23  14109  gsumvalfi  14132  opprringb  14362  rrgmex  14545  aprprop  14577  lssmex  14667  lidlmex  14787  2idlmex  14813  df2idl2  14821  2idlss  14826  isbasis3g  15073  innei  15190  cnpnei  15246  cncnp2m  15258  cnptopresti  15265  cnptoprest2  15267  imasnopn  15326  xmettx  15537  cdivcncfap  15631  expcncf  15636  cnopnap  15638  ivthinclemdisj  15667  dvrecap  15740  dvmptfsum  15752  logfac  15921  gausslemma2dlem0i  16093  gausslemma2dlem1a  16094  2lgslem1c  16126  2sqlem10  16161  lfgredg2dom  16290  ausgrusgrben  16326  ausgrumgrien  16328  ausgrusgrien  16329  uspgredg2vlem  16378  uspgredg2v  16379  usgredg2vlem2  16381  ushgredgedg  16384  ushgredgedgloop  16386  griedg0ssusgr  16409  vtxedgfi  16447  vtxlpfi  16448  wlk1walkdom  16517  wlk0prc  16530  clwwlknonex2  16597  eupthi  16607  ex-ceil  16657  bj-nnbist  16689  bj-con1st  16696  bj-charfunbi  16754  bj-sucexg  16865  bj-om  16880  bj-inf2vnlem1  16913  trilpolemisumle  16995  cndcap  17017  als-no-surprise  17055