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

Theorem bi2anan9 916
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 740 . 2 (𝜑 → ((𝜓𝜏) ↔ (𝜒𝜏)))
3 bi2an9.2 . . 3 (𝜃 → (𝜏𝜂))
43anbi2d 739 . 2 (𝜃 → ((𝜒𝜏) ↔ (𝜒𝜂)))
52, 4sylan9bb 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:  bi2anan9r  917  2reu5  3403  ralprg  4210  raltpg  4212  prssg  4323  prsspwg  4328  ssprss  4329  opelopab2a  4955  opelxp  5111  eqrel  5175  eqrelrel  5187  brcog  5253  tpres  6421  dff13  6467  resoprab2  6711  ovig  6736  dfoprab4f  7174  f1o2ndf1  7231  om00el  7602  oeoe  7625  eroveu  7788  endisj  7992  infxpen  8782  dfac5lem4  8894  sornom  9044  ltsrpr  9843  axcnre  9930  axmulgt0  10057  wloglei  10505  mulge0b  10838  addltmul  11213  ltxr  11893  fzadd2  12315  sumsqeq0  12879  rlim  14155  cpnnen  14878  dvds2lem  14913  opoe  15006  omoe  15007  opeo  15008  omeo  15009  gcddvds  15144  dfgcd2  15182  pcqmul  15477  xpsfrnel2  16141  eqgval  17559  frgpuplem  18101  mpfind  19450  2ndcctbss  21163  txbasval  21314  cnmpt12  21375  cnmpt22  21382  prdsxmslem2  22239  ishtpy  22674  bcthlem1  23024  bcth  23029  volun  23215  vitali  23283  itg1addlem3  23366  rolle  23652  mumullem2  24801  lgsquadlem3  25002  lgsquad  25003  2sqlem7  25044  axpasch  25716  wlkson  26415  iswwlksnon  26603  frgr2wwlk1  27046  numclwwlkovg  27070  numclwwlkovh  27083  hlimi  27885  leopadd  28831  eqrelrd2  29260  isinftm  29512  metidv  29709  altopthg  31708  altopthbg  31709  brsegle  31849  finxpreclem3  32854  itg2addnclem3  33081  prtlem13  33619  dib1dim  35920  pellex  36865  prsprel  41013
  Copyright terms: Public domain W3C validator