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

Theorem bibi2d 318
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  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
bibi2d  |-  ( ph  ->  ( ( th  <->  ps )  <->  ( th  <->  ch ) ) )

Proof of Theorem bibi2d
StepHypRef Expression
1 imbid.1 . . . . 5  |-  ( ph  ->  ( ps  <->  ch )
)
21pm5.74i 247 . . . 4  |-  ( (
ph  ->  ps )  <->  ( ph  ->  ch ) )
32bibi2i 313 . . 3  |-  ( ( ( ph  ->  th )  <->  (
ph  ->  ps ) )  <-> 
( ( ph  ->  th )  <->  ( ph  ->  ch ) ) )
4 pm5.74 246 . . 3  |-  ( (
ph  ->  ( th  <->  ps )
)  <->  ( ( ph  ->  th )  <->  ( ph  ->  ps ) ) )
5 pm5.74 246 . . 3  |-  ( (
ph  ->  ( th  <->  ch )
)  <->  ( ( ph  ->  th )  <->  ( ph  ->  ch ) ) )
63, 4, 53bitr4i 279 . 2  |-  ( (
ph  ->  ( th  <->  ps )
)  <->  ( ph  ->  ( th  <->  ch ) ) )
76pm5.74ri 248 1  |-  ( ph  ->  ( ( th  <->  ps )  <->  ( th  <->  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 186
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 187
This theorem is referenced by:  bibi1d  319  bibi12d  321  biantr  934  bimsc1  941  eujust  2242  eujustALT  2243  euf  2250  reu6i  3242  sbc2or  3288  axrep1  4510  axrep2  4511  axrep3  4512  zfrepclf  4515  axsep2  4520  zfauscl  4521  copsexg  4678  euotd  4693  cnveq0  5282  iotaval  5546  iota5  5555  eufnfv  6129  isoeq1  6200  isoeq3  6202  isores2  6214  isores3  6216  isotr  6217  isoini2  6220  riota5f  6266  caovordg  6465  caovord  6469  dfoprab4f  6844  seqomlem2  7155  xpf1o  7719  aceq0  8533  dfac5  8543  zfac  8874  zfcndrep  9024  zfcndac  9029  ltasr  9509  axpre-ltadd  9576  absmod0  13287  absz  13295  smuval2  14343  prmdvdsexp  14466  isacs2  15269  isacs1i  15273  mreacs  15274  abvfval  17789  abvpropd  17813  isclo2  19884  t0sep  20120  kqt0lem  20531  r0sep  20543  iccpnfcnv  21738  rolle  22685  fargshiftfo  25067  2wlkeq  25136  ismndo2  25774  eigre  27180  fgreu  27969  fcnvgreu  27970  xrge0iifcnv  28381  cvmlift2lem13  29625  iota5f  29944  nn0prpwlem  30563  nn0prpw  30564  bj-axrep1  30951  bj-axrep2  30952  bj-axrep3  30953  bj-axsep2  31070  islaut  33113  ispautN  33129  mrefg2  35014  zindbi  35256  jm2.19lem3  35308  iotavalb  36198
  Copyright terms: Public domain W3C validator