Theorem bi2anan9 606

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  bi2anan9r  607  rspc2gv  2877  ralprg  3670  raltpg  3672  prssg  3776  prsspwg  3779  opelopab2a  4296  opelxp  4690  eqrel  4749  eqrelrel  4761  brcog  4830  dff13  5812  resoprab2  6016  ovig  6041  dfoprab4f  6248  f1o2ndf1  6283  eroveu  6682  th3qlem1  6693  th3qlem2  6694  th3q  6696  oviec  6697  endisj  6880  exmidapne  7322  dfplpq2  7416  dfmpq2  7417  ordpipqqs  7436  enq0enq  7493  mulnnnq0  7512  ltsrprg  7809  axcnre  7943  axmulgt0  8093  addltmul  9222  ltxr  9844  sumsqeq0  10692  mul0inf  11387  dvds2lem  11949  opoe  12039  omoe  12040  opeo  12041  omeo  12042  gcddvds  12103  dfgcd2  12154  pcqmul  12444  xpsfrnel2  12932  eqgval  13296  txbasval  14446  cnmpt12  14466  cnmpt22  14473  lgsquadlem3  15236  lgsquad  15237  2sqlem7  15278