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

Theorem baibd 539
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 528 . . 3 (𝜒 → (𝜃 ↔ (𝜒𝜃)))
32bicomd 223 . 2 (𝜒 → ((𝜒𝜃) ↔ 𝜃))
41, 3sylan9bb 509 1 ((𝜑𝜒) → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395
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 207  df-an 396
This theorem is referenced by:  rbaibd  540  pw2f1olem  9116  eluz  12892  elicc4  13454  s111  14653  limsupgle  15513  lo1resb  15600  o1resb  15602  isercolllem2  15702  divalgmodcl  16444  ismri2  17675  acsfiel2  17698  eqglact  19197  eqgid  19198  cntzel  19341  dprdsubg  20044  subgdmdprd  20054  dprd2da  20062  dmdprdpr  20069  issubrg3  20600  ishil2  21739  obslbs  21750  iscld2  23036  isperf3  23161  cncnp2  23289  cnnei  23290  trfbas2  23851  flimrest  23991  flfnei  23999  fclsrest  24032  tsmssubm  24151  isnghm2  24745  isnghm3  24746  isnmhm2  24773  iscfil2  25300  caucfil  25317  ellimc2  25912  cnlimc  25923  lhop1  26053  dvfsumlem1  26066  fsumharmonic  27055  fsumvma  27257  fsumvma2  27258  vmasum  27260  chpchtsum  27263  chpub  27264  rpvmasum2  27556  dchrisum0lem1  27560  dirith  27573  uvtx2vtx1edg  29415  uvtx2vtx1edgb  29416  iscplgrnb  29433  frgr3v  30294  adjeu  31908  suppiniseg  32695  suppss3  32735  nndiffz1  32788  indpreima  32850  islinds5  33395  fsumcvg4  33949  qqhval2lem  33982  eulerpartlemf  34372  elorvc  34462  hashreprin  34635  neibastop3  36363  relowlpssretop  37365  sstotbnd2  37781  isbnd3b  37792  lshpkr  39118  isat2  39288  islln4  39509  islpln4  39533  islvol4  39576  islhp2  39999  pw2f1o2val2  43052  modelaxreplem3  44997  rfcnpre1  45024  rfcnpre2  45036  joindm3  48866  meetdm3  48868  catprsc  48902
  Copyright terms: Public domain W3C validator