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

Theorem biimpi 119
Description: Infer an implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
biimpi.1 (𝜑𝜓)
Assertion
Ref Expression
biimpi (𝜑𝜓)

Proof of Theorem biimpi
StepHypRef Expression
1 biimpi.1 . 2 (𝜑𝜓)
2 bi1 117 . 2 ((𝜑𝜓) → (𝜑𝜓))
31, 2ax-mp 5 1 (𝜑𝜓)
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  751  pm2.32  758  oranim  770  stabnot  818  exmiddc  821  pm2.1dc  822  stdcndcOLD  831  stdcn  832  imanst  873  pm5.75  946  rnlem  960  simp1bi  996  simp2bi  997  simp3bi  998  syl3an1b  1252  syl3an2b  1253  syl3an3b  1254  exalim  1478  nford  1546  stdpc5  1563  sbbii  1738  sb9i  1955  eu5  2046  exmoeudc  2062  eqeq1  2146  eleq2  2203  nner  2312  rexalim  2430  gencbvex  2732  gencbval  2734  moeq  2859  euind  2871  reuind  2889  ssel  3091  ssrmof  3160  unssd  3252  ssind  3300  unssdif  3311  ss0  3403  prprc  3633  disjnim  3920  trint  4041  snexprc  4110  undifexmid  4117  exmidn0m  4124  exmidsssn  4125  exmidundif  4129  exmidundifim  4130  pocl  4225  sotritrieq  4247  frirrg  4272  unexg  4364  abnex  4368  reusv3i  4380  ordtriexmid  4437  ordtri2orexmid  4438  preleq  4470  0elsucexmid  4480  ordpwsucexmid  4485  ordtri2or2exmid  4486  elnn  4519  brrelex12  4577  0nelrel  4585  elrel  4641  xpssres  4854  elres  4855  coi2  5055  iotabi  5097  uniabio  5098  nfunv  5156  funun  5167  funcnv3  5185  funimass1  5200  imain  5205  funssxp  5292  f0dom0  5316  f1o00  5402  fsn2  5594  isoselem  5721  oprabid  5803  brabvv  5817  oprssdmm  6069  1stdm  6080  f1o2ndf1  6125  poxp  6129  rdgon  6283  frecfcllem  6301  nntri3or  6389  nntri1  6392  ensym  6675  xpen  6739  snnen2oprc  6754  phplem4on  6761  fict  6762  fidceq  6763  infiexmid  6771  php5fin  6776  fisbth  6777  fin0  6779  fin0or  6780  diffisn  6787  infnfi  6789  en2eqpr  6801  exmidpw  6802  fientri3  6803  unsnfi  6807  unsnfidcex  6808  unsnfidcel  6809  undifdcss  6811  ssfidc  6823  relcnvfi  6829  fiuni  6866  eqinfti  6907  djulclb  6940  updjud  6967  omp1eomlem  6979  0ct  6992  ctmlemr  6993  ctssdclemn0  6995  ctssdccl  6996  enomnilem  7010  finomni  7012  exmidomni  7014  enq0sym  7252  enq0tr  7254  prarloclem3  7317  nqprl  7371  nqpru  7372  addnqprlemrl  7377  addnqprlemru  7378  addnqprlemfl  7379  addnqprlemfu  7380  mulnqprlemrl  7393  mulnqprlemru  7394  mulnqprlemfl  7395  mulnqprlemfu  7396  ltexprlemfl  7429  ltexprlemfu  7431  recexprlemopl  7445  recexprlemopu  7447  aptipr  7461  cauappcvgprlemladdfu  7474  cauappcvgprlemladdfl  7475  caucvgprlemladdfu  7497  caucvgprprlemexbt  7526  suplocexprlemrl  7537  suplocexprlemru  7539  suplocexprlemex  7542  srpospr  7603  elrealeu  7649  axarch  7711  axcaucvglemres  7719  nn0ge2m1nn  9049  elnn0z  9079  peano2z  9102  uzm1  9368  qapne  9443  rpregt0  9467  rpnegap  9486  npnflt  9610  nmnfgt  9613  xaddf  9639  xaddval  9640  xltadd1  9671  xsubge0  9676  xleaddadd  9682  elfz1end  9847  1fv  9928  elfzonlteqm1  9999  qtri3or  10032  exbtwnzlemshrink  10038  rebtwn2zlemshrink  10043  ioom  10050  modfzo0difsn  10180  modsumfzodifsn  10181  addmodlteq  10183  frecfzennn  10211  seq3f1olemstep  10286  ser0  10299  exp3vallem  10306  facp1  10488  faclbnd  10499  bcn1  10516  hashennnuni  10537  hashcl  10539  hashfz1  10541  hashen  10542  fihashdom  10561  hashun  10563  zfz1isolem1  10595  zfz1iso  10596  sqrt0  10788  resqrexlemfp1  10793  cau3lem  10898  xrmaxifle  11027  xrmaxiflemval  11031  xrmaxltsup  11039  xrmaxadd  11042  climserle  11126  climcaucn  11132  iserabs  11256  isumshft  11271  cvgratgt0  11314  mertenslem2  11317  prodf1  11323  eirrap  11495  bezoutlemzz  11701  dfgcd3  11709  lcmcllem  11759  prmind2  11812  prm2orodd  11818  sqrt2irr0  11853  sqrt2irrap  11869  ennnfonelemjn  11926  ennnfonelemdm  11944  ennnfonelemim  11948  ctiunctlemfo  11963  isstructr  11988  isbasis3g  12227  innei  12346  cnpnei  12402  cncnp2m  12414  cnptopresti  12421  cnptoprest2  12423  imasnopn  12482  xmettx  12693  cdivcncfap  12770  expcncf  12775  cnopnap  12777  ivthinclemdisj  12801  dvrecap  12860  ex-ceil  12997  bj-nnbist  13012  bj-sucexg  13179  bj-om  13194  bj-inf2vnlem1  13227  exmid1stab  13254  trilpolemisumle  13292
  Copyright terms: Public domain W3C validator