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

Theorem baibd 909
Description: Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
Hypothesis
Ref Expression
baibd.1
Assertion
Ref Expression
baibd

Proof of Theorem baibd
StepHypRef Expression
1 baibd.1 . 2
2 ibar 504 . . 3
32bicomd 201 . 2
41, 3sylan9bb 699 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369
This theorem is referenced by:  pw2f1olem  7641  eluz  11123  elicc4  11620  s111  12623  limsupgle  13300  lo1resb  13387  o1resb  13389  isercolllem2  13488  ismri2  15029  acsfiel2  15052  issect2  15149  eqglact  16252  eqgid  16253  cntzel  16361  dprdsubg  17071  subgdmdprd  17081  dprd2da  17091  dmdprdpr  17098  issubrg3  17457  ishil2  18750  obslbs  18761  iscld2  19529  isperf3  19654  cncnp2  19782  cnnei  19783  trfbas2  20344  flimrest  20484  flfnei  20492  fclsrest  20525  tsmssubm  20644  isnghm2  21231  isnghm3  21232  isnmhm2  21259  iscfil2  21705  caucfil  21722  ellimc2  22281  cnlimc  22292  lhop1  22415  dvfsumlem1  22427  fsumharmonic  23341  fsumvma  23488  fsumvma2  23489  vmasum  23491  chpchtsum  23494  chpub  23495  rpvmasum2  23697  dchrisum0lem1  23701  dirith  23714  cusgrauvtxb  24496  adjeu  26808  suppss3  27550  nndiffz1  27596  fsumcvg4  27932  qqhval2lem  27962  indpreima  28038  eulerpartlemf  28309  elorvc  28398  neibastop3  30180  sstotbnd2  30270  isbnd3b  30281  pw2f1o2val2  30982  rfcnpre1  31394  rfcnpre2  31406  lshpkr  34842  isat2  35012  islln4  35231  islpln4  35255  islvol4  35298  islhp2  35721
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
  Copyright terms: Public domain W3C validator