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

Theorem bibi1d 226
 Description: Deduction adding a biconditional to the right in an equivalence. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
imbid.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
bibi1d (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))

Proof of Theorem bibi1d
StepHypRef Expression
1 imbid.1 . . 3 (𝜑 → (𝜓𝜒))
21bibi2d 225 . 2 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
3 bicom 132 . 2 ((𝜓𝜃) ↔ (𝜃𝜓))
4 bicom 132 . 2 ((𝜒𝜃) ↔ (𝜃𝜒))
52, 3, 43bitr4g 216 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 102 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  bibi12d  228  bibi1  233  biassdc  1302  eubidh  1922  eubid  1923  axext3  2039  bm1.1  2041  eqeq1  2062  pm13.183  2704  elabgt  2707  elrab3t  2720  mob  2746  sbctt  2852  sbcabel  2867  isoeq2  5470  caovcang  5690  expap0  9450  bdsepnft  10394  bdsepnfALT  10396  strcollnft  10496  strcollnfALT  10498
 Copyright terms: Public domain W3C validator