Theorem bi2anan9 570

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

Syntax hints:   -> wi 4   /\ wa 102   <-> wb 103

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  bi2anan9r  571  rspc2gv  2712  ralprg  3443  raltpg  3445  prssg  3542  prsspwg  3544  opelopab2a  4020  opelxp  4392  eqrel  4447  eqrelrel  4459  brcog  4520  dff13  5428  resoprab2  5618  ovig  5642  dfoprab4f  5839  f1o2ndf1  5869  eroveu  6220  th3qlem1  6231  th3qlem2  6232  th3q  6234  oviec  6235  endisj  6321  dfplpq2  6544  dfmpq2  6545  ordpipqqs  6564  enq0enq  6621  mulnnnq0  6640  ltsrprg  6924  axcnre  7047  axmulgt0  7184  addltmul  8267  ltxr  8849  sumsqeq0  9554  dvds2lem  10207  opoe  10295  omoe  10296  opeo  10297  omeo  10298  gcddvds  10355  dfgcd2  10403