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  6966  eluz  10241  elicc4  10717  s111  11448  limsupgle  11951  lo1resb  12038  o1resb  12040  isercolllem2  12139  ismri2  13534  acsfiel2  13557  issect2  13657  isfull  13784  isfth  13788  eqglact  14668  eqgid  14669  cntzel  14799  dprdsubg  15259  subgdmdprd  15269  dprd2da  15277  dmdprdpr  15284  issubrg3  15573  ishil2  16619  obslbs  16630  iscld2  16765  isperf3  16884  cncnp2  17010  trfbas2  17538  flimrest  17678  flfnei  17686  fclsrest  17719  tsmssubm  17825  isnghm2  18233  isnghm3  18234  isnmhm2  18261  iscfil2  18692  caucfil  18709  ellimc2  19227  cnlimc  19238  lhop1  19361  dvfsumlem1  19373  fsumharmonic  20305  fsumvma  20452  fsumvma2  20453  vmasum  20455  chpchtsum  20458  chpub  20459  rpvmasum2  20661  dchrisum0lem1  20665  dirith  20678  adjeu  22469  indpreima  23608  elorvc  23660  plimfil  25558  ismonb1  25811  isepib1  25821  issubcatb  25847  neibastop3  26311  sstotbnd2  26498  isbnd3b  26509  pw2f1o2val2  27133  rfcnpre1  27690  rfcnpre2  27702  lshpkr  29307  isat2  29477  islln4  29696  islpln4  29720  islvol4  29763  islhp2  30186
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