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

Theorem bi2anan9 873
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  874  2eu6OLD  2384  2reu5  3308  ralprg  4081  raltpg  4083  prssg  4187  prsspwg  4189  opelopab2a  4771  opelxp  5038  eqrel  5101  eqrelrel  5113  brcog  5179  tpres  6125  dff13  6167  resoprab2  6398  ovig  6423  dfoprab4f  6857  f1o2ndf1  6907  om00el  7243  oeoe  7266  eroveu  7424  endisj  7623  infxpen  8409  dfac5lem4  8524  sornom  8674  ltsrpr  9471  axcnre  9558  axmulgt0  9676  wloglei  10106  mulge0b  10433  addltmul  10795  ltxr  11349  sumsqeq0  12249  rlim  13330  cpnnen  13974  dvds2lem  14008  gcddvds  14165  opoe  14347  omoe  14348  opeo  14349  omeo  14350  pcqmul  14389  xpsfrnel2  14982  eqgval  16377  frgpuplem  16917  mpfind  18332  2ndcctbss  20082  txbasval  20233  cnmpt12  20294  cnmpt22  20301  prdsxmslem2  21158  ishtpy  21598  bcthlem1  21889  bcth  21894  volun  22081  vitali  22148  itg1addlem3  22231  rolle  22517  mumullem2  23580  lgsquadlem3  23757  lgsquad  23758  2sqlem7  23771  axpasch  24371  usgra2adedgwlkonALT  24743  usgra2wlkspthlem1  24746  el2wlkonotot1  25001  frg2wot1  25184  frg2woteqm  25186  numclwwlkovg  25214  hlimi  26232  leopadd  27178  eqrelrd2  27610  isinftm  27885  metidv  28032  altopthg  29822  altopthbg  29823  brsegle  29963  itg2addnclem3  30273  fzadd2  30439  prtlem13  30814  pellex  30975  dib1dim  37035
  Copyright terms: Public domain W3C validator