Theorem bi2anan9 576

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bi2anan9r  577  rspc2gv  2755  ralprg  3521  raltpg  3523  prssg  3624  prsspwg  3626  opelopab2a  4125  opelxp  4507  eqrel  4566  eqrelrel  4578  brcog  4644  dff13  5601  resoprab2  5800  ovig  5824  dfoprab4f  6021  f1o2ndf1  6055  eroveu  6450  th3qlem1  6461  th3qlem2  6462  th3q  6464  oviec  6465  endisj  6647  dfplpq2  7063  dfmpq2  7064  ordpipqqs  7083  enq0enq  7140  mulnnnq0  7159  ltsrprg  7443  axcnre  7566  axmulgt0  7708  addltmul  8808  ltxr  9403  sumsqeq0  10212  mul0inf  10851  dvds2lem  11300  opoe  11387  omoe  11388  opeo  11389  omeo  11390  gcddvds  11447  dfgcd2  11495  txbasval  12217  cnmpt12  12237  cnmpt22  12244