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  4407  opelxp  4804  eqrel  4864  eqrelrel  4876  brcog  4947  dff13  5974  resoprab2  6185  ovig  6210  dfoprab4f  6427  f1o2ndf1  6464  eroveu  6900  th3qlem1  6911  th3qlem2  6912  th3q  6914  oviec  6915  endisj  7122  exmidapne  7626  dfplpq2  7721  dfmpq2  7722  ordpipqqs  7741  enq0enq  7798  mulnnnq0  7817  ltsrprg  8114  axcnre  8248  axmulgt0  8397  addltmul  9542  ltxr  10177  sumsqeq0  11055  ccat0  11364  mul0inf  12007  dvds2lem  12570  opoe  12662  omoe  12663  opeo  12664  omeo  12665  gcddvds  12740  dfgcd2  12791  pcqmul  13082  xpsfrnel2  13667  eqgval  14026  txbasval  15368  cnmpt12  15388  cnmpt22  15395  lgsquadlem3  16198  lgsquad  16199  2sqlem7  16240