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

Theorem baibd 875
Description: Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
Hypothesis
Ref Expression
baibd.1  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
th ) ) )
Assertion
Ref Expression
baibd  |-  ( (
ph  /\  ch )  ->  ( ps  <->  th )
)

Proof of Theorem baibd
StepHypRef Expression
1 baibd.1 . 2  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
th ) ) )
2 ibar 490 . . 3  |-  ( ch 
->  ( th  <->  ( ch  /\ 
th ) ) )
32bicomd 192 . 2  |-  ( ch 
->  ( ( ch  /\  th )  <->  th ) )
41, 3sylan9bb 680 1  |-  ( (
ph  /\  ch )  ->  ( ps  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  pw2f1olem  6982  eluz  10257  elicc4  10733  s111  11464  limsupgle  11967  lo1resb  12054  o1resb  12056  isercolllem2  12155  ismri2  13550  acsfiel2  13573  issect2  13673  isfull  13800  isfth  13804  eqglact  14684  eqgid  14685  cntzel  14815  dprdsubg  15275  subgdmdprd  15285  dprd2da  15293  dmdprdpr  15300  issubrg3  15589  ishil2  16635  obslbs  16646  iscld2  16781  isperf3  16900  cncnp2  17026  trfbas2  17554  flimrest  17694  flfnei  17702  fclsrest  17735  tsmssubm  17841  isnghm2  18249  isnghm3  18250  isnmhm2  18277  iscfil2  18708  caucfil  18725  ellimc2  19243  cnlimc  19254  lhop1  19377  dvfsumlem1  19389  fsumharmonic  20321  fsumvma  20468  fsumvma2  20469  vmasum  20471  chpchtsum  20474  chpub  20475  rpvmasum2  20677  dchrisum0lem1  20681  dirith  20694  adjeu  22485  indpreima  23623  elorvc  23675  plimfil  25661  ismonb1  25914  isepib1  25924  issubcatb  25950  neibastop3  26414  sstotbnd2  26601  isbnd3b  26612  pw2f1o2val2  27236  rfcnpre1  27793  rfcnpre2  27805  lshpkr  29929  isat2  30099  islln4  30318  islpln4  30342  islvol4  30385  islhp2  30808
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 177  df-an 360
  Copyright terms: Public domain W3C validator