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

Theorem bibi2d 343
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 271 . . . 4 ((𝜑𝜓) ↔ (𝜑𝜒))
32bibi2i 338 . . 3 (((𝜑𝜃) ↔ (𝜑𝜓)) ↔ ((𝜑𝜃) ↔ (𝜑𝜒)))
4 pm5.74 270 . . 3 ((𝜑 → (𝜃𝜓)) ↔ ((𝜑𝜃) ↔ (𝜑𝜓)))
5 pm5.74 270 . . 3 ((𝜑 → (𝜃𝜒)) ↔ ((𝜑𝜃) ↔ (𝜑𝜒)))
63, 4, 53bitr4i 303 . 2 ((𝜑 → (𝜃𝜓)) ↔ (𝜑 → (𝜃𝜒)))
76pm5.74ri 272 1 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205
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 206
This theorem is referenced by:  bibi1d  344  bibi12d  346  biantr  805  eujust  2570  eujustALT  2571  euf  2575  reu6i  3687  sbc2or  3749  axrep1  5244  axreplem  5245  zfrepclf  5252  axsepg  5258  zfauscl  5259  notzfaus  5319  copsexgw  5448  copsexg  5449  euotd  5471  cnveq0  6150  iotavalOLD  6471  iota5  6480  eufnfv  7180  isoeq1  7263  isoeq3  7265  isores2  7279  isores3  7281  isotr  7282  isoini2  7285  riota5f  7343  caovordg  7562  caovord  7566  dfoprab4f  7989  seqomlem2  8398  xpf1o  9084  aceq0  10055  dfac5  10065  zfac  10397  zfcndrep  10551  zfcndac  10556  ltasr  11037  axpre-ltadd  11104  absmod0  15189  absz  15197  smuval2  16363  prmdvdsexp  16592  isacs2  17534  isacs1i  17538  mreacs  17539  abvfval  20280  abvpropd  20304  isclo2  22442  t0sep  22678  kqt0lem  23090  r0sep  23102  iccpnfcnv  24310  rolle  25357  2sqreultlem  26798  2sqreunnltlem  26801  tgjustr  27419  wlkeq  28585  eigre  30780  fgreu  31591  fcnvgreu  31592  gsumhashmul  31901  xrge0iifcnv  32517  cvmlift2lem13  33912  iota5f  34298  nn0prpwlem  34797  nn0prpw  34798  bj-zfauscl  35397  wl-eudf  36030  ismndo2  36336  islaut  38549  ispautN  38565  mrefg2  41033  zindbi  41273  jm2.19lem3  41318  oaordnr  41633  omnord1  41642  oenord1  41653  alephiso2  41837  ntrneiel2  42365  ntrneik4  42380  iotavalb  42717  eusnsn  45267  aiota0def  45335  fargshiftfo  45641  line2x  46847  eufsnlem  46914  thincciso  47076
  Copyright terms: Public domain W3C validator