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

Theorem impbida 596
Description: Deduce an equivalence from two implications. (Contributed by NM, 17-Feb-2007.)
Hypotheses
Ref Expression
impbida.1 ((𝜑𝜓) → 𝜒)
impbida.2 ((𝜑𝜒) → 𝜓)
Assertion
Ref Expression
impbida (𝜑 → (𝜓𝜒))

Proof of Theorem impbida
StepHypRef Expression
1 impbida.1 . . 3 ((𝜑𝜓) → 𝜒)
21ex 115 . 2 (𝜑 → (𝜓𝜒))
3 impbida.2 . . 3 ((𝜑𝜒) → 𝜓)
43ex 115 . 2 (𝜑 → (𝜒𝜓))
52, 4impbid 129 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  eqrdav  2176  funfvbrb  5624  f1ocnv2d  6068  1stconst  6215  2ndconst  6216  cnvf1o  6219  ersymb  6542  swoer  6556  erth  6572  enen1  6833  enen2  6834  domen1  6835  domen2  6836  xpmapenlem  6842  fidifsnen  6863  fundmfibi  6931  f1dmvrnfibi  6936  ordiso2  7027  omniwomnimkv  7158  enwomnilem  7160  nninfwlpoimlemginf  7167  infregelbex  9574  fzsplit2  10023  fseq1p1m1  10067  elfz2nn0  10085  btwnzge0  10273  modqsubdir  10366  zesq  10611  hashprg  10759  rereb  10843  abslt  11068  absle  11069  maxleastb  11194  maxltsup  11198  xrltmaxsup  11236  xrmaxltsup  11237  iserex  11318  mptfzshft  11421  fsumrev  11422  fprodrev  11598  dvdsadd2b  11818  nn0ob  11883  dfgcd3  11981  dfgcd2  11985  dvdsmulgcd  11996  lcmgcdeq  12053  isprm5  12112  qden1elz  12175  issubmnd  12722  mhmf1o  12738  grpinvid1  12801  grpinvid2  12802  0unit  13110  cncnp  13363  xmetxpbl  13641  dedekindicc  13744  coseq0q4123  13888  coseq0negpitopi  13890  relogeftb  13919  relogbcxpbap  14016  pwf1oexmid  14371  isomninnlem  14401  apdiff  14419  iswomninnlem  14420  ismkvnnlem  14423  redcwlpolemeq1  14425
  Copyright terms: Public domain W3C validator