ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  bibi2d Structured version   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  858  bimsc1  869  eujust  1899  euf  1902  ceqex  2665  reu6i  2726  axsep2  3867  zfauscl  3868  copsexg  3972  euotd  3982  cnveq0  4720  iotaval  4821  iota5  4830  eufnfv  5332  isoeq1  5384  isoeq3  5386  isores2  5396  isores3  5398  isotr  5399  isoini2  5401  riota5f  5435  caovordg  5610  caovord  5614  dfoprab4f  5761  nnaword  6020  ltanqg  6384  ltmnqg  6385  ltasrg  6678  axpre-ltadd  6750  bdsep2  9320  bdzfauscl  9324  strcoll2  9413  sscoll2  9418
  Copyright terms: Public domain W3C validator