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

Theorem biimpi 113
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 111 . 2 ((φψ) → (φψ))
31, 2ax-mp 7 1 (φψ)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  sylbi  114  biimpri  124  sylib  127  mpbi  133  syl5bi  141  syl6ib  150  syl7bi  154  syl8ib  155  bitri  173  simplbi  259  simprbi  260  sylanb  268  sylan2b  271  anc2l  310  orbi2i  666  pm2.32  673  stabnot  729  exmiddc  732  pm2.1dc  733  oranim  795  stabtestimpdc  812  pm5.75  855  rnlem  869  simp1bi  905  simp2bi  906  simp3bi  907  syl3an1b  1155  syl3an2b  1156  syl3an3b  1157  exalim  1368  nford  1437  stdpc5  1454  sbbii  1626  sb9i  1834  eu5  1925  exmoeudc  1941  eqeq1  2024  eleq2  2079  nner  2188  rexalim  2293  gencbvex  2573  gencbval  2575  moeq  2689  euind  2701  reuind  2717  eqsbc3r  2792  ssel  2912  unssd  3092  ssind  3134  unssdif  3145  ss0  3230  prprc  3450  trint  3839  snexprc  3908  pocl  4010  sotritrieq  4032  unexg  4124  reusv3i  4137  ordtriexmid  4190  ordtri2orexmid  4191  preleq  4213  ordpwsucexmid  4226  elnn  4251  brrelex12  4304  elrel  4365  xpssres  4568  elres  4569  coi2  4760  iotabi  4799  uniabio  4800  nfunv  4855  funun  4866  funcnv3  4883  funimass1  4898  imain  4903  funssxp  4981  f1o00  5082  fsn2  5258  isoselem  5380  oprabid  5457  brabvv  5470  1stdm  5727  f1o2ndf1  5768  poxp  5771  nntri3or  5983  nntri1  5985  enq0sym  6281  enq0tr  6283  prarloclem3  6345  ltexprlemfl  6440  ltexprlemfu  6442  recexprlemopl  6453  recexprlemopu  6455  bj-sucexg  7284  bj-om  7298  bj-inf2vnlem1  7327
  Copyright terms: Public domain W3C validator