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

Theorem bibi2d 332
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 327 . . 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  333  bibi12d  335  biantr  971  bimsc1  979  eujust  2471  eujustALT  2472  euf  2477  reu6i  3384  sbc2or  3431  axrep1  4742  axrep2  4743  axrep3  4744  zfrepclf  4747  axsep2  4752  zfauscl  4753  copsexg  4926  euotd  4945  cnveq0  5560  iotaval  5831  iota5  5840  eufnfv  6456  isoeq1  6532  isoeq3  6534  isores2  6548  isores3  6550  isotr  6551  isoini2  6554  riota5f  6601  caovordg  6806  caovord  6810  dfoprab4f  7186  seqomlem2  7506  xpf1o  8082  aceq0  8901  dfac5  8911  zfac  9242  zfcndrep  9396  zfcndac  9401  ltasr  9881  axpre-ltadd  9948  absmod0  13993  absz  14001  smuval2  15147  prmdvdsexp  15370  isacs2  16254  isacs1i  16258  mreacs  16259  abvfval  18758  abvpropd  18782  isclo2  20832  t0sep  21068  kqt0lem  21479  r0sep  21491  iccpnfcnv  22683  rolle  23691  wlkeq  26433  eigre  28582  fgreu  29355  fcnvgreu  29356  xrge0iifcnv  29803  cvmlift2lem13  31058  iota5f  31368  nn0prpwlem  32012  nn0prpw  32013  bj-axrep1  32484  bj-axrep2  32485  bj-axrep3  32486  bj-axsep2  32621  wl-eudf  33025  ismndo2  33344  islaut  34888  ispautN  34904  mrefg2  36789  zindbi  37030  jm2.19lem3  37077  ntrneiel2  37905  ntrneik4  37920  iotavalb  38152  fargshiftfo  40706
  Copyright terms: Public domain W3C validator