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

Theorem bibi1d 231
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 230 . 2 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
3 bicom 138 . 2 ((𝜓𝜃) ↔ (𝜃𝜓))
4 bicom 138 . 2 ((𝜒𝜃) ↔ (𝜃𝜒))
52, 3, 43bitr4g 221 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  bibi12d  233  bibi1  238  biassdc  1331  eubidh  1954  eubid  1955  axext3  2071  bm1.1  2073  eqeq1  2094  pm13.183  2752  elabgt  2755  elrab3t  2768  mob  2795  sbctt  2903  sbcabel  2918  isoeq2  5563  caovcang  5788  frecabcl  6146  expap0  9950  bezoutlemeu  11089  dfgcd3  11092  bezout  11093  prmdvdsexp  11220  bdsepnft  11435  bdsepnfALT  11437  strcollnft  11536  strcollnfALT  11538
  Copyright terms: Public domain W3C validator