Theorem bi2anan9 571

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 453	. 2 |- ( ph -> ( ( ps /\ ta ) <-> ( ch /\ ta ) ) )
3		bi2an9.2	. . 3 |- ( th -> ( ta <-> et ) )
4	3	anbi2d 452	. 2 |- ( th -> ( ( ch /\ ta ) <-> ( ch /\ et ) ) )
5	2, 4	sylan9bb 450	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  572  rspc2gv  2720  ralprg  3461  raltpg  3463  prssg  3562  prsspwg  3564  opelopab2a  4048  opelxp  4420  eqrel  4475  eqrelrel  4487  brcog  4550  dff13  5459  resoprab2  5649  ovig  5673  dfoprab4f  5870  f1o2ndf1  5900  eroveu  6284  th3qlem1  6295  th3qlem2  6296  th3q  6298  oviec  6299  endisj  6389  dfplpq2  6658  dfmpq2  6659  ordpipqqs  6678  enq0enq  6735  mulnnnq0  6754  ltsrprg  7038  axcnre  7161  axmulgt0  7303  addltmul  8386  ltxr  8979  sumsqeq0  9703  dvds2lem  10415  opoe  10502  omoe  10503  opeo  10504  omeo  10505  gcddvds  10562  dfgcd2  10610