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

Theorem baibd 876
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 491 . . 3  |-  ( ch 
->  ( th  <->  ( ch  /\ 
th ) ) )
32bicomd 193 . 2  |-  ( ch 
->  ( ( ch  /\  th )  <->  th ) )
41, 3sylan9bb 681 1  |-  ( (
ph  /\  ch )  ->  ( ps  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  pw2f1olem  7148  eluz  10431  elicc4  10909  s111  11689  limsupgle  12198  lo1resb  12285  o1resb  12287  isercolllem2  12386  ismri2  13784  acsfiel2  13807  issect2  13907  eqglact  14918  eqgid  14919  cntzel  15049  dprdsubg  15509  subgdmdprd  15519  dprd2da  15527  dmdprdpr  15534  issubrg3  15823  ishil2  16869  obslbs  16880  iscld2  17015  isperf3  17139  cncnp2  17267  cnnei  17268  trfbas2  17796  flimrest  17936  flfnei  17944  fclsrest  17977  tsmssubm  18093  isnghm2  18629  isnghm3  18630  isnmhm2  18657  iscfil2  19090  caucfil  19107  ellimc2  19631  cnlimc  19642  lhop1  19765  dvfsumlem1  19777  fsumharmonic  20717  fsumvma  20864  fsumvma2  20865  vmasum  20867  chpchtsum  20870  chpub  20871  rpvmasum2  21073  dchrisum0lem1  21077  dirith  21090  cusgrauvtxb  21371  adjeu  23240  qqhval2lem  24164  indpreima  24218  elorvc  24496  neibastop3  26082  sstotbnd2  26174  isbnd3b  26185  pw2f1o2val2  26802  rfcnpre1  27358  rfcnpre2  27370  lshpkr  29232  isat2  29402  islln4  29621  islpln4  29645  islvol4  29688  islhp2  30111
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  df-an 361
  Copyright terms: Public domain W3C validator