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-1 5  ax-2 6  ax-mp 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  1332  eubidh  1955  eubid  1956  axext3  2072  bm1.1  2074  eqeq1  2095  pm13.183  2755  elabgt  2758  elrab3t  2771  mob  2798  sbctt  2906  sbcabel  2921  isoeq2  5595  caovcang  5820  frecabcl  6178  expap0  10046  bezoutlemeu  11335  dfgcd3  11338  bezout  11339  prmdvdsexp  11466  bdsepnft  12051  bdsepnfALT  12053  strcollnft  12152  strcollnfALT  12154
  Copyright terms: Public domain W3C validator