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

Theorem bibi2d 310
Description: Deduction adding a biconditional to the left in an equivalence. (Contributed by NM, 5-Aug-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 237 . . . 4  |-  ( (
ph  ->  ps )  <->  ( ph  ->  ch ) )
32bibi2i 305 . . 3  |-  ( ( ( ph  ->  th )  <->  (
ph  ->  ps ) )  <-> 
( ( ph  ->  th )  <->  ( ph  ->  ch ) ) )
4 pm5.74 236 . . 3  |-  ( (
ph  ->  ( th  <->  ps )
)  <->  ( ( ph  ->  th )  <->  ( ph  ->  ps ) ) )
5 pm5.74 236 . . 3  |-  ( (
ph  ->  ( th  <->  ch )
)  <->  ( ( ph  ->  th )  <->  ( ph  ->  ch ) ) )
63, 4, 53bitr4i 269 . 2  |-  ( (
ph  ->  ( th  <->  ps )
)  <->  ( ph  ->  ( th  <->  ch ) ) )
76pm5.74ri 238 1  |-  ( ph  ->  ( ( th  <->  ps )  <->  ( th  <->  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  bibi1d  311  bibi12d  313  biantr  898  bimsc1  905  eujust  2282  eujustALT  2283  euf  2286  ceqex  3058  reu6i  3117  sbc2or  3161  axrep1  4313  axrep2  4314  axrep3  4315  zfrepclf  4318  axsep2  4323  zfauscl  4324  copsexg  4434  euotd  4449  cnveq0  5319  iotaval  5421  iota5  5430  eufnfv  5964  isoeq1  6031  isoeq3  6033  isores2  6045  isores3  6047  isotr  6048  isoini2  6051  caovordg  6246  caovord  6250  dfoprab4f  6397  riota5f  6566  seqomlem2  6700  xpf1o  7261  aceq0  7991  dfac5  8001  zfac  8332  zfcndrep  8481  zfcndac  8486  ltasr  8967  axpre-ltadd  9034  absmod0  12100  absz  12108  smuval2  12986  prmdvdsexp  13106  isacs2  13870  isacs1i  13874  mreacs  13875  abvfval  15898  abvpropd  15922  isclo2  17144  t0sep  17380  kqt0lem  17760  r0sep  17772  iccpnfcnv  18961  rolle  19866  fargshiftfo  21617  ismndo2  21925  eigre  23330  xrge0iifcnv  24311  cvmlift2lem13  24994  iota5f  25174  nn0prpwlem  26316  nn0prpw  26317  mrefg2  26752  zindbi  27000  jm2.19lem3  27053  iotavalb  27598  islaut  30817  ispautN  30833
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator