Theorem bi2anan9 601

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bi2anan9r  602  rspc2gv  2846  ralprg  3634  raltpg  3636  prssg  3737  prsspwg  3739  opelopab2a  4250  opelxp  4641  eqrel  4700  eqrelrel  4712  brcog  4778  dff13  5747  resoprab2  5950  ovig  5974  dfoprab4f  6172  f1o2ndf1  6207  eroveu  6604  th3qlem1  6615  th3qlem2  6616  th3q  6618  oviec  6619  endisj  6802  dfplpq2  7316  dfmpq2  7317  ordpipqqs  7336  enq0enq  7393  mulnnnq0  7412  ltsrprg  7709  axcnre  7843  axmulgt0  7991  addltmul  9114  ltxr  9732  sumsqeq0  10554  mul0inf  11204  dvds2lem  11765  opoe  11854  omoe  11855  opeo  11856  omeo  11857  gcddvds  11918  dfgcd2  11969  pcqmul  12257  txbasval  13061  cnmpt12  13081  cnmpt22  13088  2sqlem7  13751