Theorem bi2anan9 614

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 469	. 2 |- ( ph -> ( ( ps /\ ta ) <-> ( ch /\ ta ) ) )
3		bi2an9.2	. . 3 |- ( th -> ( ta <-> et ) )
4	3	anbi2d 468	. 2 |- ( th -> ( ( ch /\ ta ) <-> ( ch /\ et ) ) )
5	2, 4	sylan9bb 466	1 |- ( ( ph /\ th ) -> ( ( ps /\ ta ) <-> ( ch /\ et ) ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  bi2anan9r  615  rspc2gv  2942  ralprg  3760  raltpg  3762  prssg  3872  prsspwg  3875  ssprss  3876  opelopab2a  4409  opelxp  4806  eqrel  4866  eqrelrel  4878  brcog  4949  dff13  5977  resoprab2  6188  ovig  6213  dfoprab4f  6431  f1o2ndf1  6468  eroveu  6905  th3qlem1  6916  th3qlem2  6917  th3q  6919  oviec  6920  endisj  7128  exmidapne  7632  dfplpq2  7727  dfmpq2  7728  ordpipqqs  7747  enq0enq  7804  mulnnnq0  7823  ltsrprg  8120  axcnre  8254  axmulgt0  8403  addltmul  9553  ltxr  10193  sumsqeq0  11075  ccat0  11385  mul0inf  12031  dvds2lem  12594  opoe  12686  omoe  12687  opeo  12688  omeo  12689  gcddvds  12764  dfgcd2  12815  pcqmul  13110  xpsfrnel2  13725  eqgval  14084  txbasval  15510  cnmpt12  15530  cnmpt22  15537  lgsquadlem3  16420  lgsquad  16421  2sqlem7  16462