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

Step	Hyp	Ref	Expression
1		bi2an9.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	anbi1d 704	. 2 |- ( ph -> ( ( ps /\ ta ) <-> ( ch /\ ta ) ) )
3		bi2an9.2	. . 3 |- ( th -> ( ta <-> et ) )
4	3	anbi2d 703	. 2 |- ( th -> ( ( ch /\ ta ) <-> ( ch /\ et ) ) )
5	2, 4	sylan9bb 699	1 |- ( ( ph /\ th ) -> ( ( ps /\ ta ) <-> ( ch /\ et ) ) )

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