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

Theorem bi2anan9 637
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 . 2 (𝜑 → (𝜓𝜒))
2 bi2an9.2 . 2 (𝜃 → (𝜏𝜂))
3 pm4.38 636 . 2 (((𝜓𝜒) ∧ (𝜏𝜂)) → ((𝜓𝜏) ↔ (𝜒𝜂)))
41, 2, 3syl2an 596 1 ((𝜑𝜃) → ((𝜓𝜏) ↔ (𝜒𝜂)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396
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 206  df-an 397
This theorem is referenced by:  bi2anan9r  638  rspc2gv  3587  2reu5  3714  ralprgf  4651  ralprg  4653  raltpg  4657  prssg  4777  prsspwg  4781  ssprss  4782  intprg  4940  opelopab2a  5490  opelxp  5667  eqrel  5738  eqrelrel  5751  brcog  5820  tpres  7146  dff13  7198  resoprab2  7469  ovig  7495  dfoprab4f  7980  f1o2ndf1  8046  om00el  8515  oeoe  8538  eroveu  8709  endisj  8960  infxpen  9908  dfac5lem4  10020  sornom  10171  ltsrpr  10971  axcnre  11058  axmulgt0  11187  wloglei  11645  mulge0b  11983  addltmul  12347  ltxr  12990  fzadd2  13430  sumsqeq0  14035  ccat0  14417  rlim  15336  cpnnen  16070  dvds2lem  16110  opoe  16204  omoe  16205  opeo  16206  omeo  16207  gcddvds  16342  dfgcd2  16386  pcqmul  16684  xpsfrnel2  17405  eqgval  18937  frgpuplem  19512  mpfind  21468  2ndcctbss  22757  txbasval  22908  cnmpt12  22969  cnmpt22  22976  prdsxmslem2  23836  ishtpy  24286  bcthlem1  24639  bcth  24644  volun  24860  vitali  24928  itg1addlem3  25013  rolle  25305  mumullem2  26480  lgsquadlem3  26681  lgsquad  26682  2sqlem7  26723  scutval  27090  slerec  27109  axpasch  27718  wlkson  28432  iswwlksnon  28626  wpthswwlks2on  28734  eulplig  29255  hlimi  29958  leopadd  30902  eqrelrd2  31362  cntzun  31726  isinftm  31841  finexttrb  32164  metidv  32276  satfv1  33760  satfbrsuc  33763  gonarlem  33791  satfv0fvfmla0  33810  satfv1fvfmla1  33820  altopthg  34483  altopthbg  34484  brsegle  34624  bj-imdirvallem  35582  finxpreclem3  35795  itg2addnclem3  36062  exan3  36686  exanres  36687  exanres3  36688  eqrel2  36691  brcoss  36824  brcoss3  36826  brcoels  36828  br1cossxrnres  36841  brcosscnv  36865  prtlem13  37261  dib1dim  39559  pellex  41060  prsprel  45573  uspgrsprf1  45943  uspgrsprfo  45944
  Copyright terms: Public domain W3C validator