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

Theorem bibi2d 346
 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 274 . . . 4 ((𝜑𝜓) ↔ (𝜑𝜒))
32bibi2i 341 . . 3 (((𝜑𝜃) ↔ (𝜑𝜓)) ↔ ((𝜑𝜃) ↔ (𝜑𝜒)))
4 pm5.74 273 . . 3 ((𝜑 → (𝜃𝜓)) ↔ ((𝜑𝜃) ↔ (𝜑𝜓)))
5 pm5.74 273 . . 3 ((𝜑 → (𝜃𝜒)) ↔ ((𝜑𝜃) ↔ (𝜑𝜒)))
63, 4, 53bitr4i 306 . 2 ((𝜑 → (𝜃𝜓)) ↔ (𝜑 → (𝜃𝜒)))
76pm5.74ri 275 1 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209 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 210 This theorem is referenced by:  bibi1d  347  bibi12d  349  biantr  805  eujust  2590  eujustALT  2591  euf  2595  reu6i  3642  sbc2or  3705  axrep1  5157  axreplem  5158  zfrepclf  5164  axsepg  5170  zfauscl  5171  notzfaus  5230  copsexgw  5349  copsexg  5350  euotd  5372  cnveq0  6026  iotaval  6309  iota5  6318  eufnfv  6983  isoeq1  7064  isoeq3  7066  isores2  7080  isores3  7082  isotr  7083  isoini2  7086  riota5f  7136  caovordg  7351  caovord  7355  dfoprab4f  7758  seqomlem2  8097  xpf1o  8701  aceq0  9578  dfac5  9588  zfac  9920  zfcndrep  10074  zfcndac  10079  ltasr  10560  axpre-ltadd  10627  absmod0  14711  absz  14719  smuval2  15881  prmdvdsexp  16111  isacs2  16982  isacs1i  16986  mreacs  16987  abvfval  19657  abvpropd  19681  isclo2  21788  t0sep  22024  kqt0lem  22436  r0sep  22448  iccpnfcnv  23645  rolle  24689  2sqreultlem  26130  2sqreunnltlem  26133  tgjustr  26367  wlkeq  27522  eigre  29717  fgreu  30533  fcnvgreu  30534  gsumhashmul  30842  xrge0iifcnv  31404  cvmlift2lem13  32793  iota5f  33187  nn0prpwlem  34060  nn0prpw  34061  bj-zfauscl  34648  wl-eudf  35253  ismndo2  35592  islaut  37659  ispautN  37675  mrefg2  40021  zindbi  40260  jm2.19lem3  40305  alephiso2  40630  ntrneiel2  41162  ntrneik4  41177  iotavalb  41507  eusnsn  43984  aiota0def  44019  fargshiftfo  44327  line2x  45533
 Copyright terms: Public domain W3C validator