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  4106  zfauscl  4107  copsexg  4227  euotd  4237  cnveq0  5065  iotaval  5169  iota5  5178  eufnfv  5723  isoeq1  5777  isoeq3  5779  isores2  5789  isores3  5791  isotr  5792  isoini2  5795  riota5f  5830  caovordg  6017  caovord  6021  dfoprab4f  6169  frecabcl  6375  nnaword  6487  xpf1o  6818  ltanqg  7349  ltmnqg  7350  ltasrg  7719  axpre-ltadd  7835  prmdvdsexp  12089  bdsep2  13881  bdzfauscl  13885
  Copyright terms: Public domain W3C validator