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

Theorem baibd 947
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 525 . . 3 (𝜒 → (𝜃 ↔ (𝜒𝜃)))
32bicomd 213 . 2 (𝜒 → ((𝜒𝜃) ↔ 𝜃))
41, 3sylan9bb 735 1 ((𝜑𝜒) → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  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 197  df-an 386
This theorem is referenced by:  pw2f1olem  8011  eluz  11648  elicc4  12185  s111  13337  limsupgle  14145  lo1resb  14232  o1resb  14234  isercolllem2  14333  divalgmodcl  15058  ismri2  16216  acsfiel2  16240  issect2  16338  eqglact  17569  eqgid  17570  cntzel  17680  dprdsubg  18347  subgdmdprd  18357  dprd2da  18365  dmdprdpr  18372  issubrg3  18732  ishil2  19985  obslbs  19996  iscld2  20745  isperf3  20870  cncnp2  20998  cnnei  20999  trfbas2  21560  flimrest  21700  flfnei  21708  fclsrest  21741  tsmssubm  21859  isnghm2  22441  isnghm3  22442  isnmhm2  22469  iscfil2  22977  caucfil  22994  ellimc2  23554  cnlimc  23565  lhop1  23688  dvfsumlem1  23700  fsumharmonic  24645  fsumvma  24845  fsumvma2  24846  vmasum  24848  chpchtsum  24851  chpub  24852  rpvmasum2  25108  dchrisum0lem1  25112  dirith  25125  uvtx2vtx1edg  26193  uvtx2vtx1edgb  26194  iscplgrnb  26206  frgr3v  27010  adjeu  28609  suppss3  29357  nndiffz1  29402  fsumcvg4  29790  qqhval2lem  29819  indpreima  29880  eulerpartlemf  30225  elorvc  30314  neibastop3  32020  relowlpssretop  32865  sstotbnd2  33226  isbnd3b  33237  lshpkr  33905  isat2  34075  islln4  34294  islpln4  34318  islvol4  34361  islhp2  34784  pw2f1o2val2  37108  rfcnpre1  38682  rfcnpre2  38694
  Copyright terms: Public domain W3C validator