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  947  bimsc1  958  eujust  2021  euf  2024  ceqex  2857  reu6i  2921  axsep2  4108  zfauscl  4109  copsexg  4229  euotd  4239  cnveq0  5067  iotaval  5171  iota5  5180  eufnfv  5726  isoeq1  5780  isoeq3  5782  isores2  5792  isores3  5794  isotr  5795  isoini2  5798  riota5f  5833  caovordg  6020  caovord  6024  dfoprab4f  6172  frecabcl  6378  nnaword  6490  xpf1o  6822  ltanqg  7362  ltmnqg  7363  ltasrg  7732  axpre-ltadd  7848  prmdvdsexp  12102  bdsep2  13921  bdzfauscl  13925
  Copyright terms: Public domain W3C validator