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

Theorem bibi1d 233
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 232 . 2 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
3 bicom 140 . 2 ((𝜓𝜃) ↔ (𝜃𝜓))
4 bicom 140 . 2 ((𝜒𝜃) ↔ (𝜃𝜒))
52, 3, 43bitr4g 223 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  bibi12d  235  bibi1  240  biassdc  1406  eubidh  2044  eubid  2045  axext3  2172  bm1.1  2174  eqeq1  2196  pm13.183  2890  elabgt  2893  elrab3t  2907  mob  2934  sbctt  3044  sbcabel  3059  isoeq2  5819  caovcang  6053  frecabcl  6418  expap0  10568  bezoutlemeu  12026  dfgcd3  12029  bezout  12030  prmdvdsexp  12166  ismet  14241  isxmet  14242  bdsepnft  15036  bdsepnfALT  15038
  Copyright terms: Public domain W3C validator