Theorem bi2anan9 614

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  bi2anan9r  615  rspc2gv  2942  ralprg  3760  raltpg  3762  prssg  3872  prsspwg  3875  ssprss  3876  opelopab2a  4409  opelxp  4806  eqrel  4866  eqrelrel  4878  brcog  4949  dff13  5977  resoprab2  6188  ovig  6213  dfoprab4f  6431  f1o2ndf1  6468  eroveu  6904  th3qlem1  6915  th3qlem2  6916  th3q  6918  oviec  6919  endisj  7126  exmidapne  7632  dfplpq2  7727  dfmpq2  7728  ordpipqqs  7747  enq0enq  7804  mulnnnq0  7823  ltsrprg  8120  axcnre  8254  axmulgt0  8403  addltmul  9553  ltxr  10194  sumsqeq0  11076  ccat0  11386  mul0inf  12032  dvds2lem  12595  opoe  12687  omoe  12688  opeo  12689  omeo  12690  gcddvds  12765  dfgcd2  12816  pcqmul  13111  xpsfrnel2  13726  eqgval  14085  txbasval  15493  cnmpt12  15513  cnmpt22  15520  lgsquadlem3  16403  lgsquad  16404  2sqlem7  16445