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  2889  ralprg  3684  raltpg  3686  prssg  3790  prsspwg  3793  opelopab2a  4312  opelxp  4706  eqrel  4765  eqrelrel  4777  brcog  4846  dff13  5839  resoprab2  6044  ovig  6069  dfoprab4f  6281  f1o2ndf1  6316  eroveu  6715  th3qlem1  6726  th3qlem2  6727  th3q  6729  oviec  6730  endisj  6921  exmidapne  7374  dfplpq2  7469  dfmpq2  7470  ordpipqqs  7489  enq0enq  7546  mulnnnq0  7565  ltsrprg  7862  axcnre  7996  axmulgt0  8146  addltmul  9276  ltxr  9899  sumsqeq0  10765  ccat0  11055  mul0inf  11585  dvds2lem  12147  opoe  12239  omoe  12240  opeo  12241  omeo  12242  gcddvds  12317  dfgcd2  12368  pcqmul  12659  xpsfrnel2  13211  eqgval  13592  txbasval  14772  cnmpt12  14792  cnmpt22  14799  lgsquadlem3  15589  lgsquad  15590  2sqlem7  15631