Theorem bi2anan9 610

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  611  rspc2gv  2922  ralprg  3720  raltpg  3722  prssg  3830  prsspwg  3833  ssprss  3834  opelopab2a  4359  opelxp  4755  eqrel  4815  eqrelrel  4827  brcog  4897  dff13  5912  resoprab2  6121  ovig  6146  dfoprab4f  6359  f1o2ndf1  6396  eroveu  6798  th3qlem1  6809  th3qlem2  6810  th3q  6812  oviec  6813  endisj  7011  exmidapne  7482  dfplpq2  7577  dfmpq2  7578  ordpipqqs  7597  enq0enq  7654  mulnnnq0  7673  ltsrprg  7970  axcnre  8104  axmulgt0  8254  addltmul  9384  ltxr  10013  sumsqeq0  10884  ccat0  11180  mul0inf  11822  dvds2lem  12385  opoe  12477  omoe  12478  opeo  12479  omeo  12480  gcddvds  12555  dfgcd2  12606  pcqmul  12897  xpsfrnel2  13450  eqgval  13831  txbasval  15018  cnmpt12  15038  cnmpt22  15045  lgsquadlem3  15835  lgsquad  15836  2sqlem7  15877