ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  biimpi Unicode version

Theorem biimpi 119
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
StepHypRef Expression
1 biimpi.1 . 2  |-  ( ph  <->  ps )
2 bi1 117 . 2  |-  ( (
ph 
<->  ps )  ->  ( ph  ->  ps ) )
31, 2ax-mp 5 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  sylbi  120  sylib  121  sylbb  122  biimpri  132  mpbi  144  syl5bi  151  syl6ib  160  syl7bi  164  syl8ib  165  bitri  183  simplbi  272  simprbi  273  sylanb  282  sylan2b  285  anc2l  325  sylanblc  411  orbi2i  736  pm2.32  743  oranim  755  stabnot  803  exmiddc  806  pm2.1dc  807  stdcndcOLD  816  stdcn  817  imanst  858  pm5.75  931  rnlem  945  simp1bi  981  simp2bi  982  simp3bi  983  syl3an1b  1237  syl3an2b  1238  syl3an3b  1239  exalim  1463  nford  1531  stdpc5  1548  sbbii  1723  sb9i  1933  eu5  2024  exmoeudc  2040  eqeq1  2124  eleq2  2181  nner  2289  rexalim  2407  gencbvex  2706  gencbval  2708  moeq  2832  euind  2844  reuind  2862  ssel  3061  ssrmof  3130  unssd  3222  ssind  3270  unssdif  3281  ss0  3373  prprc  3603  disjnim  3890  trint  4011  snexprc  4080  undifexmid  4087  exmidn0m  4094  exmidsssn  4095  exmidundif  4099  exmidundifim  4100  pocl  4195  sotritrieq  4217  frirrg  4242  unexg  4334  abnex  4338  reusv3i  4350  ordtriexmid  4407  ordtri2orexmid  4408  preleq  4440  0elsucexmid  4450  ordpwsucexmid  4455  ordtri2or2exmid  4456  elnn  4489  brrelex12  4547  0nelrel  4555  elrel  4611  xpssres  4824  elres  4825  coi2  5025  iotabi  5067  uniabio  5068  nfunv  5126  funun  5137  funcnv3  5155  funimass1  5170  imain  5175  funssxp  5262  f0dom0  5286  f1o00  5370  fsn2  5562  isoselem  5689  oprabid  5771  brabvv  5785  oprssdmm  6037  1stdm  6048  f1o2ndf1  6093  poxp  6097  rdgon  6251  frecfcllem  6269  nntri3or  6357  nntri1  6360  ensym  6643  xpen  6707  snnen2oprc  6722  phplem4on  6729  fict  6730  fidceq  6731  infiexmid  6739  php5fin  6744  fisbth  6745  fin0  6747  fin0or  6748  diffisn  6755  infnfi  6757  en2eqpr  6769  exmidpw  6770  fientri3  6771  unsnfi  6775  unsnfidcex  6776  unsnfidcel  6777  undifdcss  6779  ssfidc  6791  relcnvfi  6797  fiuni  6834  eqinfti  6875  djulclb  6908  updjud  6935  omp1eomlem  6947  0ct  6960  ctmlemr  6961  ctssdclemn0  6963  ctssdccl  6964  enomnilem  6978  finomni  6980  exmidomni  6982  enq0sym  7208  enq0tr  7210  prarloclem3  7273  nqprl  7327  nqpru  7328  addnqprlemrl  7333  addnqprlemru  7334  addnqprlemfl  7335  addnqprlemfu  7336  mulnqprlemrl  7349  mulnqprlemru  7350  mulnqprlemfl  7351  mulnqprlemfu  7352  ltexprlemfl  7385  ltexprlemfu  7387  recexprlemopl  7401  recexprlemopu  7403  aptipr  7417  cauappcvgprlemladdfu  7430  cauappcvgprlemladdfl  7431  caucvgprlemladdfu  7453  caucvgprprlemexbt  7482  suplocexprlemrl  7493  suplocexprlemru  7495  suplocexprlemex  7498  srpospr  7559  elrealeu  7605  axarch  7667  axcaucvglemres  7675  nn0ge2m1nn  9005  elnn0z  9035  peano2z  9058  uzm1  9324  qapne  9399  rpregt0  9423  rpnegap  9442  npnflt  9566  nmnfgt  9569  xaddf  9595  xaddval  9596  xltadd1  9627  xsubge0  9632  xleaddadd  9638  elfz1end  9803  1fv  9884  elfzonlteqm1  9955  qtri3or  9988  exbtwnzlemshrink  9994  rebtwn2zlemshrink  9999  ioom  10006  modfzo0difsn  10136  modsumfzodifsn  10137  addmodlteq  10139  frecfzennn  10167  seq3f1olemstep  10242  ser0  10255  exp3vallem  10262  facp1  10444  faclbnd  10455  bcn1  10472  hashennnuni  10493  hashcl  10495  hashfz1  10497  hashen  10498  fihashdom  10517  hashun  10519  zfz1isolem1  10551  zfz1iso  10552  sqrt0  10744  resqrexlemfp1  10749  cau3lem  10854  xrmaxifle  10983  xrmaxiflemval  10987  xrmaxltsup  10995  xrmaxadd  10998  climserle  11082  climcaucn  11088  iserabs  11212  isumshft  11227  cvgratgt0  11270  mertenslem2  11273  eirrap  11411  bezoutlemzz  11617  dfgcd3  11625  lcmcllem  11675  prmind2  11728  prm2orodd  11734  sqrt2irr0  11769  sqrt2irrap  11785  ennnfonelemjn  11842  ennnfonelemdm  11860  ennnfonelemim  11864  ctiunctlemfo  11879  isstructr  11901  isbasis3g  12140  innei  12259  cnpnei  12315  cncnp2m  12327  cnptopresti  12334  cnptoprest2  12336  imasnopn  12395  xmettx  12606  cdivcncfap  12683  expcncf  12688  cnopnap  12690  ivthinclemdisj  12714  dvrecap  12773  ex-ceil  12865  bj-nnbist  12880  bj-sucexg  13047  bj-om  13062  bj-inf2vnlem1  13095  exmid1stab  13122  trilpolemisumle  13158
  Copyright terms: Public domain W3C validator