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

Theorem impbida 585
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 114 . 2 (𝜑 → (𝜓𝜒))
3 impbida.2 . . 3 ((𝜑𝜒) → 𝜓)
43ex 114 . 2 (𝜑 → (𝜒𝜓))
52, 4impbid 128 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  eqrdav  2138  funfvbrb  5533  f1ocnv2d  5974  1stconst  6118  2ndconst  6119  cnvf1o  6122  ersymb  6443  swoer  6457  erth  6473  enen1  6734  enen2  6735  domen1  6736  domen2  6737  xpmapenlem  6743  fidifsnen  6764  fundmfibi  6827  f1dmvrnfibi  6832  ordiso2  6920  fzsplit2  9837  fseq1p1m1  9881  elfz2nn0  9899  btwnzge0  10080  modqsubdir  10173  zesq  10417  hashprg  10561  rereb  10642  abslt  10867  absle  10868  maxleastb  10993  maxltsup  10997  xrltmaxsup  11033  xrmaxltsup  11034  iserex  11115  mptfzshft  11218  fsumrev  11219  dvdsadd2b  11547  nn0ob  11612  dfgcd3  11705  dfgcd2  11709  dvdsmulgcd  11720  lcmgcdeq  11771  qden1elz  11890  cncnp  12409  xmetxpbl  12687  dedekindicc  12790  coseq0q4123  12928  coseq0negpitopi  12930  relogeftb  12957  pwf1oexmid  13224  isomninnlem  13255  apdiff  13269
  Copyright terms: Public domain W3C validator