ILE Home 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  5267  f1ocnv2d  5691  1stconst  5829  2ndconst  5830  cnvf1o  5833  ersymb  6107  swoer  6121  erth  6137  enen1  6298  enen2  6299  domen1  6300  domen2  6301  fidifsnen  6318  fzsplit2  8881  fseq1p1m1  8923  elfz2nn0  8940  zesq  9245  rereb  9341  abslt  9562  absle  9563  iiserex  9736
  Copyright terms: Public domain W3C validator