ILE Home 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-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:  bibi1d  232  bibi12d  234  biantr  921  bimsc1  932  eujust  1979  euf  1982  ceqex  2786  reu6i  2848  axsep2  4017  zfauscl  4018  copsexg  4136  euotd  4146  cnveq0  4965  iotaval  5069  iota5  5078  eufnfv  5616  isoeq1  5670  isoeq3  5672  isores2  5682  isores3  5684  isotr  5685  isoini2  5688  riota5f  5722  caovordg  5906  caovord  5910  dfoprab4f  6059  frecabcl  6264  nnaword  6375  xpf1o  6706  ltanqg  7176  ltmnqg  7177  ltasrg  7546  axpre-ltadd  7662  prmdvdsexp  11753  bdsep2  13011  bdzfauscl  13015  strcoll2  13108  sscoll2  13113
  Copyright terms: Public domain W3C validator