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

Theorem bibi2d 225
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 173 . . . 4 ((𝜑𝜓) ↔ (𝜑𝜒))
32bibi2i 220 . . 3 (((𝜑𝜃) ↔ (𝜑𝜓)) ↔ ((𝜑𝜃) ↔ (𝜑𝜒)))
4 pm5.74 172 . . 3 ((𝜑 → (𝜃𝜓)) ↔ ((𝜑𝜃) ↔ (𝜑𝜓)))
5 pm5.74 172 . . 3 ((𝜑 → (𝜃𝜒)) ↔ ((𝜑𝜃) ↔ (𝜑𝜒)))
63, 4, 53bitr4i 205 . 2 ((𝜑 → (𝜃𝜓)) ↔ (𝜑 → (𝜃𝜒)))
76pm5.74ri 174 1 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  bibi1d  226  bibi12d  228  biantr  870  bimsc1  881  eujust  1918  euf  1921  ceqex  2694  reu6i  2755  axsep2  3904  zfauscl  3905  copsexg  4009  euotd  4019  cnveq0  4805  iotaval  4906  iota5  4915  eufnfv  5417  isoeq1  5469  isoeq3  5471  isores2  5481  isores3  5483  isotr  5484  isoini2  5486  riota5f  5520  caovordg  5696  caovord  5700  dfoprab4f  5847  nnaword  6115  ltanqg  6556  ltmnqg  6557  ltasrg  6913  axpre-ltadd  7018  bdsep2  10393  bdzfauscl  10397  strcoll2  10495  sscoll2  10500
  Copyright terms: Public domain W3C validator