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  936  bimsc1  947  eujust  2001  euf  2004  ceqex  2812  reu6i  2875  axsep2  4047  zfauscl  4048  copsexg  4166  euotd  4176  cnveq0  4995  iotaval  5099  iota5  5108  eufnfv  5648  isoeq1  5702  isoeq3  5704  isores2  5714  isores3  5716  isotr  5717  isoini2  5720  riota5f  5754  caovordg  5938  caovord  5942  dfoprab4f  6091  frecabcl  6296  nnaword  6407  xpf1o  6738  ltanqg  7220  ltmnqg  7221  ltasrg  7590  axpre-ltadd  7706  prmdvdsexp  11837  bdsep2  13189  bdzfauscl  13193  strcoll2  13286  sscoll2  13291
  Copyright terms: Public domain W3C validator