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

Theorem bibi2d 221
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 169 . . . 4 ((𝜑𝜓) ↔ (𝜑𝜒))
32bibi2i 216 . . 3 (((𝜑𝜃) ↔ (𝜑𝜓)) ↔ ((𝜑𝜃) ↔ (𝜑𝜒)))
4 pm5.74 168 . . 3 ((𝜑 → (𝜃𝜓)) ↔ ((𝜑𝜃) ↔ (𝜑𝜓)))
5 pm5.74 168 . . 3 ((𝜑 → (𝜃𝜒)) ↔ ((𝜑𝜃) ↔ (𝜑𝜒)))
63, 4, 53bitr4i 201 . 2 ((𝜑 → (𝜃𝜓)) ↔ (𝜑 → (𝜃𝜒)))
76pm5.74ri 170 1 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  bibi1d  222  bibi12d  224  biantr  859  bimsc1  870  eujust  1902  euf  1905  ceqex  2668  reu6i  2729  axsep2  3873  zfauscl  3874  copsexg  3978  euotd  3988  cnveq0  4764  iotaval  4865  iota5  4874  eufnfv  5376  isoeq1  5428  isoeq3  5430  isores2  5440  isores3  5442  isotr  5443  isoini2  5445  riota5f  5479  caovordg  5655  caovord  5659  dfoprab4f  5806  nnaword  6071  ltanqg  6479  ltmnqg  6480  ltasrg  6836  axpre-ltadd  6941  bdsep2  9879  bdzfauscl  9883  strcoll2  9981  sscoll2  9986
  Copyright terms: Public domain W3C validator