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

Theorem bi2anan9 871
Description: Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 31-Jul-1995.)
Hypotheses
Ref Expression
bi2an9.1  |-  ( ph  ->  ( ps  <->  ch )
)
bi2an9.2  |-  ( th 
->  ( ta  <->  et )
)
Assertion
Ref Expression
bi2anan9  |-  ( (
ph  /\  th )  ->  ( ( ps  /\  ta )  <->  ( ch  /\  et ) ) )

Proof of Theorem bi2anan9
StepHypRef Expression
1 bi2an9.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21anbi1d 704 . 2  |-  ( ph  ->  ( ( ps  /\  ta )  <->  ( ch  /\  ta ) ) )
3 bi2an9.2 . . 3  |-  ( th 
->  ( ta  <->  et )
)
43anbi2d 703 . 2  |-  ( th 
->  ( ( ch  /\  ta )  <->  ( ch  /\  et ) ) )
52, 4sylan9bb 699 1  |-  ( (
ph  /\  th )  ->  ( ( ps  /\  ta )  <->  ( ch  /\  et ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  bi2anan9r  872  2eu6OLD  2368  2reu5  3292  ralprg  4059  raltpg  4061  prssg  4166  prsspwg  4168  opelopab2a  4748  opelxp  5015  eqrel  5078  eqrelrel  5090  brcog  5155  dff13  6147  resoprab2  6380  ovig  6405  dfoprab4f  6839  f1o2ndf1  6889  om00el  7223  oeoe  7246  eroveu  7404  endisj  7602  infxpen  8390  dfac5lem4  8505  sornom  8655  ltsrpr  9452  axcnre  9539  axmulgt0  9657  wloglei  10086  mulge0b  10413  addltmul  10775  ltxr  11328  sumsqeq0  12220  rlim  13292  cpnnen  13834  dvds2lem  13868  gcddvds  14025  opoe  14207  omoe  14208  opeo  14209  omeo  14210  pcqmul  14249  xpsfrnel2  14834  eqgval  16119  frgpuplem  16659  mpfind  18073  2ndcctbss  19822  txbasval  19973  cnmpt12  20034  cnmpt22  20041  prdsxmslem2  20898  ishtpy  21338  bcthlem1  21629  bcth  21634  volun  21821  vitali  21888  itg1addlem3  21971  rolle  22257  mumullem2  23319  lgsquadlem3  23496  lgsquad  23497  2sqlem7  23510  axpasch  24109  usgra2adedgwlkonALT  24481  usgra2wlkspthlem1  24484  el2wlkonotot1  24739  frg2wot1  24922  frg2woteqm  24924  numclwwlkovg  24952  hlimi  25970  leopadd  26916  eqrelrd2  27332  isinftm  27591  metidv  27737  altopthg  29585  altopthbg  29586  brsegle  29726  itg2addnclem3  30036  fzadd2  30202  prtlem13  30577  pellex  30739  tpres  32386  dib1dim  36594
  Copyright terms: Public domain W3C validator