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

Theorem impbida 538
 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 112 . 2 (𝜑 → (𝜓𝜒))
3 impbida.2 . . 3 ((𝜑𝜒) → 𝜓)
43ex 112 . 2 (𝜑 → (𝜒𝜓))
52, 4impbid 124 1 (𝜑 → (𝜓𝜒))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101   ↔ wb 102 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 104  ax-ia3 105 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  eqrdav  2055  funfvbrb  5307  f1ocnv2d  5731  1stconst  5869  2ndconst  5870  cnvf1o  5873  ersymb  6150  swoer  6164  erth  6180  enen1  6341  enen2  6342  domen1  6343  domen2  6344  fidifsnen  6361  ordiso2  6414  fzsplit2  9015  fseq1p1m1  9057  elfz2nn0  9074  btwnzge0  9249  modqsubdir  9342  zesq  9534  rereb  9690  abslt  9914  absle  9915  iiserex  10089  dvdsadd2b  10153  nn0ob  10219
 Copyright terms: Public domain W3C validator