Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  bibi2d Structured version   Visualization version   GIF version

Theorem bibi2d 331
 Description: Deduction adding a biconditional to the left in an equivalence. (Contributed by NM, 11-May-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 260 . . . 4 ((𝜑𝜓) ↔ (𝜑𝜒))
32bibi2i 326 . . 3 (((𝜑𝜃) ↔ (𝜑𝜓)) ↔ ((𝜑𝜃) ↔ (𝜑𝜒)))
4 pm5.74 259 . . 3 ((𝜑 → (𝜃𝜓)) ↔ ((𝜑𝜃) ↔ (𝜑𝜓)))
5 pm5.74 259 . . 3 ((𝜑 → (𝜃𝜒)) ↔ ((𝜑𝜃) ↔ (𝜑𝜒)))
63, 4, 53bitr4i 292 . 2 ((𝜑 → (𝜃𝜓)) ↔ (𝜑 → (𝜃𝜒)))
76pm5.74ri 261 1 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 197 This theorem is referenced by:  bibi1d  332  bibi12d  334  biantr  1010  bimsc1  1017  eujust  2609  eujustALT  2610  euf  2615  reu6i  3538  sbc2or  3585  axrep1  4924  axrep2  4925  axrep3  4926  zfrepclf  4929  axsep2  4934  zfauscl  4935  copsexg  5104  euotd  5123  cnveq0  5749  iotaval  6023  iota5  6032  eufnfv  6655  isoeq1  6731  isoeq3  6733  isores2  6747  isores3  6749  isotr  6750  isoini2  6753  riota5f  6800  caovordg  7007  caovord  7011  dfoprab4f  7394  seqomlem2  7716  xpf1o  8289  aceq0  9151  dfac5  9161  zfac  9494  zfcndrep  9648  zfcndac  9653  ltasr  10133  axpre-ltadd  10200  absmod0  14262  absz  14270  smuval2  15426  prmdvdsexp  15649  isacs2  16535  isacs1i  16539  mreacs  16540  abvfval  19040  abvpropd  19064  isclo2  21114  t0sep  21350  kqt0lem  21761  r0sep  21773  iccpnfcnv  22964  rolle  23972  wlkeq  26760  eigre  29024  fgreu  29801  fcnvgreu  29802  xrge0iifcnv  30309  cvmlift2lem13  31625  iota5f  31934  nn0prpwlem  32644  nn0prpw  32645  bj-axrep1  33116  bj-axrep2  33117  bj-axrep3  33118  bj-axsep2  33245  bj-zfauscl  33246  wl-eudf  33685  ismndo2  34004  islaut  35890  ispautN  35906  mrefg2  37790  zindbi  38031  jm2.19lem3  38078  ntrneiel2  38904  ntrneik4  38919  iotavalb  39151  fargshiftfo  41906
 Copyright terms: Public domain W3C validator