MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  baibd Structured version   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  7204  eluz  10491  elicc4  10969  s111  11754  limsupgle  12263  lo1resb  12350  o1resb  12352  isercolllem2  12451  ismri2  13849  acsfiel2  13872  issect2  13972  eqglact  14983  eqgid  14984  cntzel  15114  dprdsubg  15574  subgdmdprd  15584  dprd2da  15592  dmdprdpr  15599  issubrg3  15888  ishil2  16938  obslbs  16949  iscld2  17084  isperf3  17209  cncnp2  17337  cnnei  17338  trfbas2  17867  flimrest  18007  flfnei  18015  fclsrest  18048  tsmssubm  18164  isnghm2  18750  isnghm3  18751  isnmhm2  18778  iscfil2  19211  caucfil  19228  ellimc2  19756  cnlimc  19767  lhop1  19890  dvfsumlem1  19902  fsumharmonic  20842  fsumvma  20989  fsumvma2  20990  vmasum  20992  chpchtsum  20995  chpub  20996  rpvmasum2  21198  dchrisum0lem1  21202  dirith  21215  cusgrauvtxb  21497  adjeu  23384  qqhval2lem  24357  indpreima  24414  elorvc  24709  neibastop3  26382  sstotbnd2  26474  isbnd3b  26485  pw2f1o2val2  27102  rfcnpre1  27657  rfcnpre2  27669  lshpkr  29852  isat2  30022  islln4  30241  islpln4  30265  islvol4  30308  islhp2  30731
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