Theorem bi2anan9 861

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 697	. 2 |- ( ph -> ( ( ps /\ ta ) <-> ( ch /\ ta ) ) )
3		bi2an9.2	. . 3 |- ( th -> ( ta <-> et ) )
4	3	anbi2d 696	. 2 |- ( th -> ( ( ch /\ ta ) <-> ( ch /\ et ) ) )
5	2, 4	sylan9bb 692	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  862  2mo  2355  2moOLD  2356  2eu6  2363  2reu5  3156  ralprg  3913  raltpg  3915  prssg  4016  prsspwg  4018  opelopab2a  4593  opelxp  4856  eqrel  4916  eqrelrel  4928  brcog  4993  dff13  5958  resoprab2  6176  ovig  6201  dfoprab4f  6621  f1o2ndf1  6669  om00el  7003  oeoe  7026  eroveu  7183  th3qlem1  7194  th3qlem2  7195  th3q  7197  ovec  7198  endisj  7386  infxpen  8169  dfac5lem4  8284  sornom  8434  ltsrpr  9232  axcnre  9319  axmulgt0  9437  wloglei  9860  mulge0b  10187  addltmul  10548  ltxr  11083  sumsqeq0  11928  rlim  12957  cpnnen  13494  dvds2lem  13528  gcddvds  13682  opoe  13861  omoe  13862  opeo  13863  omeo  13864  pcqmul  13903  xpsfrnel2  14486  eqgval  15710  frgpuplem  16249  2ndcctbss  18901  txbasval  19021  cnmpt12  19082  cnmpt22  19089  prdsxmslem2  19946  ishtpy  20386  bcthlem1  20677  bcth  20682  volun  20868  vitali  20935  itg1addlem3  21018  rolle  21304  mpfind  21396  mumullem2  22403  lgsquadlem3  22580  lgsquad  22581  2sqlem7  22594  axpasch  23010  hlimi  24413  leopadd  25359  eqrelrd2  25770  isinftm  26022  metidv  26173  altopthg  27845  altopthbg  27846  brsegle  27986  itg2addnclem3  28289  fzadd2  28481  prtlem13  28858  pellex  29021  usgra2wlkspthlem1  30142  el2wlkonotot1  30239  frg2wot1  30496  frg2woteqm  30498  numclwwlkovg  30526  dib1dim  34383