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

Theorem impbida 528
 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 108 . 2 (𝜑 → (𝜓𝜒))
3 impbida.2 . . 3 ((𝜑𝜒) → 𝜓)
43ex 108 . 2 (𝜑 → (𝜒𝜓))
52, 4impbid 120 1 (𝜑 → (𝜓𝜒))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 100  ax-ia3 101 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  eqrdav  2039  funfvbrb  5280  f1ocnv2d  5704  1stconst  5842  2ndconst  5843  cnvf1o  5846  ersymb  6120  swoer  6134  erth  6150  enen1  6311  enen2  6312  domen1  6313  domen2  6314  fidifsnen  6331  ordiso2  6357  fzsplit2  8914  fseq1p1m1  8956  elfz2nn0  8973  btwnzge0  9142  zesq  9367  rereb  9463  abslt  9684  absle  9685  iiserex  9859
 Copyright terms: Public domain W3C validator