Theorem bi2anan9 596

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

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bi2anan9r  597  rspc2gv  2842  ralprg  3627  raltpg  3629  prssg  3730  prsspwg  3732  opelopab2a  4243  opelxp  4634  eqrel  4693  eqrelrel  4705  brcog  4771  dff13  5736  resoprab2  5939  ovig  5963  dfoprab4f  6161  f1o2ndf1  6196  eroveu  6592  th3qlem1  6603  th3qlem2  6604  th3q  6606  oviec  6607  endisj  6790  dfplpq2  7295  dfmpq2  7296  ordpipqqs  7315  enq0enq  7372  mulnnnq0  7391  ltsrprg  7688  axcnre  7822  axmulgt0  7970  addltmul  9093  ltxr  9711  sumsqeq0  10533  mul0inf  11182  dvds2lem  11743  opoe  11832  omoe  11833  opeo  11834  omeo  11835  gcddvds  11896  dfgcd2  11947  pcqmul  12235  txbasval  12907  cnmpt12  12927  cnmpt22  12934  2sqlem7  13597