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  1373  eubidh  2003  eubid  2004  axext3  2120  bm1.1  2122  eqeq1  2144  pm13.183  2817  elabgt  2820  elrab3t  2834  mob  2861  sbctt  2970  sbcabel  2985  isoeq2  5696  caovcang  5925  frecabcl  6289  expap0  10316  bezoutlemeu  11684  dfgcd3  11687  bezout  11688  prmdvdsexp  11815  ismet  12502  isxmet  12503  bdsepnft  13074  bdsepnfALT  13076  strcollnft  13171  strcollnfALT  13173
 Copyright terms: Public domain W3C validator