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 )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used 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  3778  prprc  3823  disjnim  4120  trint  4246  snexprc  4325  undifexmid  4332  exmidn0m  4340  exmidsssn  4341  exmidundif  4345  exmidundifim  4346  exmid1stab  4347  pocl  4450  sotritrieq  4472  frirrg  4497  unexg  4591  abnex  4595  reusv3i  4607  ordtriexmid  4670  ontriexmidim  4671  ordtri2orexmid  4672  preleq  4704  0elsucexmid  4714  ordpwsucexmid  4719  ordtri2or2exmid  4720  elomssom  4754  brrelex12  4815  0nelrel  4823  elrel  4879  xpssres  5100  elres  5101  coi2  5307  iotabi  5350  uniabio  5351  nfunv  5413  funun  5425  funcnv3  5446  funimass1  5461  imain  5466  funssxp  5560  f0dom0  5589  f1o00  5679  fsn2  5885  funopsn  5894  isoselem  6029  oprabid  6120  brabvv  6137  uchoice  6375  oprssdmm  6409  1stdm  6420  f1o2ndf1  6468  poxp  6472  suppval1  6483  funsssuppss  6502  rdgon  6662  frecfcllem  6680  nntri3or  6771  nntri1  6774  ensym  7074  en2  7118  xpen  7151  snnen2oprc  7167  phplem4on  7175  fict  7176  fidceq  7177  infiexmid  7187  php5fin  7192  fisbth  7193  fin0  7195  fin0or  7196  diffisn  7203  infnfi  7205  fidcen  7209  en2eqpr  7220  exmidpw  7221  exmidpweq  7222  pw1fin  7223  fientri3  7228  unsnfi  7232  unsnfidcex  7233  unsnfidcel  7234  undifdcss  7236  ssfidc  7251  relcnvfi  7261  fiuni  7317  eqinfti  7366  djulclb  7401  updjud  7428  omp1eomlem  7440  0ct  7453  ctmlemr  7454  ctssdclemn0  7456  ctssdccl  7457  enomnilem  7484  finomni  7486  exmidomni  7488  enmkvlem  7507  enwomnilem  7515  exmidontriimlem1  7583  onntri35  7602  onntri52  7609  dftap2  7623  exmidapne  7632  enq0sym  7805  enq0tr  7807  prarloclem3  7870  nqprl  7924  nqpru  7925  addnqprlemrl  7930  addnqprlemru  7931  addnqprlemfl  7932  addnqprlemfu  7933  mulnqprlemrl  7946  mulnqprlemru  7947  mulnqprlemfl  7948  mulnqprlemfu  7949  ltexprlemfl  7982  ltexprlemfu  7984  recexprlemopl  7998  recexprlemopu  8000  aptipr  8014  cauappcvgprlemladdfu  8027  cauappcvgprlemladdfl  8028  caucvgprlemladdfu  8050  caucvgprprlemexbt  8079  suplocexprlemrl  8090  suplocexprlemru  8092  suplocexprlemex  8095  srpospr  8156  elrealeu  8202  axarch  8264  axcaucvglemres  8272  nn0ge2m1nn  9636  elnn0z  9666  peano2z  9689  uzm1  9968  qapne  10054  rpregt0  10084  rpnegap  10103  xnn0dcle  10220  xnn0letri  10221  npnflt  10233  nmnfgt  10236  xaddf  10262  xaddval  10263  xltadd1  10294  xsubge0  10299  xleaddadd  10305  elfz1end  10477  1fv  10562  elfzonlteqm1  10644  qtri3or  10691  exbtwnzlemshrink  10699  rebtwn2zlemshrink  10704  ioom  10711  elicore  10717  modfzo0difsn  10852  modsumfzodifsn  10853  addmodlteq  10855  frecfzennn  10883  seq3f1olemstep  10971  ser0  10990  exp3vallem  10997  facp1  11189  faclbnd  11200  bcn1  11217  hashennnuni  11239  hashcl  11241  hashfz1  11243  hashen  11244  fihashdom  11264  hashun  11266  zfz1isolem1  11313  zfz1iso  11314  lencl  11329  sswrd  11334  swrdswrd  11498  swrdccatin2  11522  pfxccat3  11527  pfxccatpfx1  11529  sqrt0  11791  resqrexlemfp1  11796  cau3lem  11902  xrmaxifle  12036  xrmaxiflemval  12040  xrmaxltsup  12048  xrmaxadd  12051  climserle  12135  climcaucn  12141  iserabs  12266  isumshft  12281  cvgratgt0  12324  mertenslem2  12327  prodf1  12333  fprodunsn  12395  fprodfac  12406  eirrap  12569  bezoutlemzz  12803  dfgcd3  12811  nnmindc  12835  nnminle  12836  nninfctlemfo  12841  lcmcllem  12869  prmind2  12922  prm2orodd  12928  sqrt2irr0  12967  sqrt2irrap  12984  ballotfilem2  13285  ballotfilemic  13307  ballotfilem1c  13308  ennnfonelemjn  13350  ennnfonelemdm  13368  ennnfonelemim  13372  ctiunctlemfo  13387  isstructr  13424  basmex  13469  dfgrp2  13890  dfgrp3mlem  13961  mulgnngzsum  13988  grpissubg  14055  ablsubsub23  14218  gsumvalfi  14241  opprringb  14494  rrgmex  14677  aprprop  14709  lssmex  14800  lidlmex  14920  2idlmex  14946  df2idl2  14954  2idlss  14959  isbasis3g  15289  innei  15406  cnpnei  15462  cncnp2m  15474  cnptopresti  15481  cnptoprest2  15483  imasnopn  15542  xmettx  15753  cdivcncfap  15847  expcncf  15852  cnopnap  15854  ivthinclemdisj  15883  dvrecap  15956  dvmptfsum  15968  logfac  16143  prmorcht  16299  gausslemma2dlem0i  16398  gausslemma2dlem1a  16399  2lgslem1c  16431  2sqlem10  16466  lfgredg2dom  16595  ausgrusgrben  16631  ausgrumgrien  16633  ausgrusgrien  16634  uspgredg2vlem  16683  uspgredg2v  16684  usgredg2vlem2  16686  ushgredgedg  16689  ushgredgedgloop  16691  griedg0ssusgr  16714  vtxedgfi  16752  vtxlpfi  16753  wlk1walkdom  16822  wlk0prc  16835  clwwlknonex2  16902  eupthi  16912  ex-ceil  16962  bj-nnbist  16994  bj-con1st  17001  bj-charfunbi  17059  bj-sucexg  17170  bj-om  17185  bj-inf2vnlem1  17218  trilpolemisumle  17311  cndcap  17333  als-no-surprise  17371