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

Theorem bibi1d 232
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 231 . 2 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
3 bicom 139 . 2 ((𝜓𝜃) ↔ (𝜃𝜓))
4 bicom 139 . 2 ((𝜒𝜃) ↔ (𝜃𝜒))
52, 3, 43bitr4g 222 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  bibi12d  234  bibi1  239  biassdc  1358  eubidh  1983  eubid  1984  axext3  2100  bm1.1  2102  eqeq1  2124  pm13.183  2796  elabgt  2799  elrab3t  2812  mob  2839  sbctt  2947  sbcabel  2962  isoeq2  5671  caovcang  5900  frecabcl  6264  expap0  10291  bezoutlemeu  11622  dfgcd3  11625  bezout  11626  prmdvdsexp  11753  ismet  12440  isxmet  12441  bdsepnft  13012  bdsepnfALT  13014  strcollnft  13109  strcollnfALT  13111
  Copyright terms: Public domain W3C validator