Theorem bi2anan9 608

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  609  rspc2gv  2919  ralprg  3717  raltpg  3719  prssg  3825  prsspwg  3828  ssprss  3829  opelopab2a  4353  opelxp  4749  eqrel  4808  eqrelrel  4820  brcog  4889  dff13  5892  resoprab2  6101  ovig  6126  dfoprab4f  6339  f1o2ndf1  6374  eroveu  6773  th3qlem1  6784  th3qlem2  6785  th3q  6787  oviec  6788  endisj  6983  exmidapne  7446  dfplpq2  7541  dfmpq2  7542  ordpipqqs  7561  enq0enq  7618  mulnnnq0  7637  ltsrprg  7934  axcnre  8068  axmulgt0  8218  addltmul  9348  ltxr  9971  sumsqeq0  10840  ccat0  11131  mul0inf  11752  dvds2lem  12314  opoe  12406  omoe  12407  opeo  12408  omeo  12409  gcddvds  12484  dfgcd2  12535  pcqmul  12826  xpsfrnel2  13379  eqgval  13760  txbasval  14941  cnmpt12  14961  cnmpt22  14968  lgsquadlem3  15758  lgsquad  15759  2sqlem7  15800