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

Theorem impbida 570
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  2116  funfvbrb  5501  f1ocnv2d  5942  1stconst  6086  2ndconst  6087  cnvf1o  6090  ersymb  6411  swoer  6425  erth  6441  enen1  6702  enen2  6703  domen1  6704  domen2  6705  xpmapenlem  6711  fidifsnen  6732  fundmfibi  6795  f1dmvrnfibi  6800  ordiso2  6888  fzsplit2  9798  fseq1p1m1  9842  elfz2nn0  9860  btwnzge0  10041  modqsubdir  10134  zesq  10378  hashprg  10522  rereb  10603  abslt  10828  absle  10829  maxleastb  10954  maxltsup  10958  xrltmaxsup  10994  xrmaxltsup  10995  iserex  11076  mptfzshft  11179  fsumrev  11180  dvdsadd2b  11467  nn0ob  11532  dfgcd3  11625  dfgcd2  11629  dvdsmulgcd  11640  lcmgcdeq  11691  qden1elz  11810  cncnp  12326  xmetxpbl  12604  dedekindicc  12707  coseq0q4123  12842  coseq0negpitopi  12844  pwf1oexmid  13121  isomninnlem  13152
  Copyright terms: Public domain W3C validator