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

Theorem baibd 535
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 524 . . 3 (𝜒 → (𝜃 ↔ (𝜒𝜃)))
32bicomd 214 . 2 (𝜒 → ((𝜒𝜃) ↔ 𝜃))
41, 3sylan9bb 505 1 ((𝜑𝜒) → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384
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 198  df-an 385
This theorem is referenced by:  pw2f1olem  8270  eluz  11899  elicc4  12441  s111  13585  limsupgle  14494  lo1resb  14581  o1resb  14583  isercolllem2  14682  divalgmodcl  15413  ismri2  16559  acsfiel2  16582  issect2  16680  eqglact  17910  eqgid  17911  cntzel  18020  dprdsubg  18689  subgdmdprd  18699  dprd2da  18707  dmdprdpr  18714  issubrg3  19076  ishil2  20338  obslbs  20349  iscld2  21111  isperf3  21236  cncnp2  21364  cnnei  21365  trfbas2  21925  flimrest  22065  flfnei  22073  fclsrest  22106  tsmssubm  22224  isnghm2  22806  isnghm3  22807  isnmhm2  22834  iscfil2  23342  caucfil  23359  ellimc2  23931  cnlimc  23942  lhop1  24067  dvfsumlem1  24079  fsumharmonic  25028  fsumvma  25228  fsumvma2  25229  vmasum  25231  chpchtsum  25234  chpub  25235  rpvmasum2  25491  dchrisum0lem1  25495  dirith  25508  uvtx2vtx1edg  26583  uvtx2vtx1edgb  26584  iscplgrnb  26602  frgr3v  27512  adjeu  29138  suppss3  29885  nndiffz1  29931  fsumcvg4  30377  qqhval2lem  30406  indpreima  30468  eulerpartlemf  30813  elorvc  30903  hashreprin  31080  neibastop3  32731  relowlpssretop  33577  sstotbnd2  33927  isbnd3b  33938  lshpkr  35005  isat2  35175  islln4  35395  islpln4  35419  islvol4  35462  islhp2  35885  pw2f1o2val2  38216  rfcnpre1  39762  rfcnpre2  39774
  Copyright terms: Public domain W3C validator