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

Theorem bibi2d 231
 Description: Deduction adding a biconditional to the left in an equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 19-May-2013.)
Hypothesis
Ref Expression
imbid.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
bibi2d (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))

Proof of Theorem bibi2d
StepHypRef Expression
1 imbid.1 . . . . 5 (𝜑 → (𝜓𝜒))
21pm5.74i 179 . . . 4 ((𝜑𝜓) ↔ (𝜑𝜒))
32bibi2i 226 . . 3 (((𝜑𝜃) ↔ (𝜑𝜓)) ↔ ((𝜑𝜃) ↔ (𝜑𝜒)))
4 pm5.74 178 . . 3 ((𝜑 → (𝜃𝜓)) ↔ ((𝜑𝜃) ↔ (𝜑𝜓)))
5 pm5.74 178 . . 3 ((𝜑 → (𝜃𝜒)) ↔ ((𝜑𝜃) ↔ (𝜑𝜒)))
63, 4, 53bitr4i 211 . 2 ((𝜑 → (𝜃𝜓)) ↔ (𝜑 → (𝜃𝜒)))
76pm5.74ri 180 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:  bibi1d  232  bibi12d  234  biantr  904  bimsc1  915  eujust  1962  euf  1965  ceqex  2766  reu6i  2828  axsep2  3987  zfauscl  3988  copsexg  4104  euotd  4114  cnveq0  4931  iotaval  5035  iota5  5044  eufnfv  5580  isoeq1  5634  isoeq3  5636  isores2  5646  isores3  5648  isotr  5649  isoini2  5652  riota5f  5686  caovordg  5870  caovord  5874  dfoprab4f  6021  frecabcl  6226  nnaword  6337  xpf1o  6667  ltanqg  7109  ltmnqg  7110  ltasrg  7466  axpre-ltadd  7571  prmdvdsexp  11619  bdsep2  12665  bdzfauscl  12669  strcoll2  12766  sscoll2  12771
 Copyright terms: Public domain W3C validator