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

Theorem bi2anan9 935
Description: Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 31-Jul-1995.)
Hypotheses
Ref Expression
bi2an9.1 (𝜑 → (𝜓𝜒))
bi2an9.2 (𝜃 → (𝜏𝜂))
Assertion
Ref Expression
bi2anan9 ((𝜑𝜃) → ((𝜓𝜏) ↔ (𝜒𝜂)))

Proof of Theorem bi2anan9
StepHypRef Expression
1 bi2an9.1 . . 3 (𝜑 → (𝜓𝜒))
21anbi1d 741 . 2 (𝜑 → ((𝜓𝜏) ↔ (𝜒𝜏)))
3 bi2an9.2 . . 3 (𝜃 → (𝜏𝜂))
43anbi2d 740 . 2 (𝜃 → ((𝜒𝜏) ↔ (𝜒𝜂)))
52, 4sylan9bb 736 1 ((𝜑𝜃) → ((𝜓𝜏) ↔ (𝜒𝜂)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383
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 385
This theorem is referenced by:  bi2anan9r  936  rspc2gv  3352  2reu5  3449  ralprg  4266  raltpg  4268  prssg  4382  prsspwg  4387  ssprss  4388  opelopab2a  5019  opelxp  5180  eqrel  5243  eqrelrel  5255  brcog  5321  tpres  6507  dff13  6552  resoprab2  6799  ovig  6824  dfoprab4f  7270  f1o2ndf1  7330  om00el  7701  oeoe  7724  eroveu  7885  endisj  8088  infxpen  8875  dfac5lem4  8987  sornom  9137  ltsrpr  9936  axcnre  10023  axmulgt0  10150  wloglei  10598  mulge0b  10931  addltmul  11306  ltxr  11987  fzadd2  12414  sumsqeq0  12982  ccat0  13394  rlim  14270  cpnnen  15002  dvds2lem  15041  opoe  15134  omoe  15135  opeo  15136  omeo  15137  gcddvds  15272  dfgcd2  15310  pcqmul  15605  xpsfrnel2  16272  eqgval  17690  frgpuplem  18231  mpfind  19584  2ndcctbss  21306  txbasval  21457  cnmpt12  21518  cnmpt22  21525  prdsxmslem2  22381  ishtpy  22818  bcthlem1  23167  bcth  23172  volun  23359  vitali  23427  itg1addlem3  23510  rolle  23798  mumullem2  24951  lgsquadlem3  25152  lgsquad  25153  2sqlem7  25194  axpasch  25866  wlkson  26608  iswwlksnon  26802  iswwlksnonOLD  26803  wpthswwlks2on  26927  numclwwlkovgOLD  27339  numclwwlkovhOLD  27362  eulplig  27467  hlimi  28173  leopadd  29119  eqrelrd2  29554  isinftm  29863  metidv  30063  scutval  32036  slerec  32048  altopthg  32199  altopthbg  32200  brsegle  32340  finxpreclem3  33360  itg2addnclem3  33593  exan3  34203  exanres  34204  exanres3  34205  eqrel2  34209  brcoss  34326  brcoss3  34328  brcoels  34330  br1cossxrnres  34338  brcosscnv  34362  prtlem13  34472  dib1dim  36771  pellex  37716  prsprel  42062  uspgrsprf1  42080  uspgrsprfo  42081
  Copyright terms: Public domain W3C validator