Theorem bi2anan9 538

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

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  bi2anan9r  539  ralprg  3421  raltpg  3423  prssg  3521  prsspwg  3523  opelopab2a  4002  opelxp  4374  eqrel  4429  eqrelrel  4441  brcog  4502  dff13  5407  resoprab2  5598  ovig  5622  dfoprab4f  5819  f1o2ndf1  5849  eroveu  6197  th3qlem1  6208  th3qlem2  6209  th3q  6211  oviec  6212  endisj  6298  dfplpq2  6452  dfmpq2  6453  ordpipqqs  6472  enq0enq  6529  mulnnnq0  6548  ltsrprg  6832  axcnre  6955  axmulgt0  7091  addltmul  8161  ltxr  8695  sumsqeq0  9332