Theorem bi2anan9 606

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  bi2anan9r  607  rspc2gv  2851  ralprg  3640  raltpg  3642  prssg  3746  prsspwg  3748  opelopab2a  4259  opelxp  4650  eqrel  4709  eqrelrel  4721  brcog  4787  dff13  5759  resoprab2  5962  ovig  5986  dfoprab4f  6184  f1o2ndf1  6219  eroveu  6616  th3qlem1  6627  th3qlem2  6628  th3q  6630  oviec  6631  endisj  6814  dfplpq2  7328  dfmpq2  7329  ordpipqqs  7348  enq0enq  7405  mulnnnq0  7424  ltsrprg  7721  axcnre  7855  axmulgt0  8003  addltmul  9128  ltxr  9746  sumsqeq0  10568  mul0inf  11217  dvds2lem  11778  opoe  11867  omoe  11868  opeo  11869  omeo  11870  gcddvds  11931  dfgcd2  11982  pcqmul  12270  txbasval  13338  cnmpt12  13358  cnmpt22  13365  2sqlem7  14028