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  2876  ralprg  3669  raltpg  3671  prssg  3775  prsspwg  3778  opelopab2a  4295  opelxp  4689  eqrel  4748  eqrelrel  4760  brcog  4829  dff13  5811  resoprab2  6015  ovig  6040  dfoprab4f  6246  f1o2ndf1  6281  eroveu  6680  th3qlem1  6691  th3qlem2  6692  th3q  6694  oviec  6695  endisj  6878  exmidapne  7320  dfplpq2  7414  dfmpq2  7415  ordpipqqs  7434  enq0enq  7491  mulnnnq0  7510  ltsrprg  7807  axcnre  7941  axmulgt0  8091  addltmul  9219  ltxr  9841  sumsqeq0  10689  mul0inf  11384  dvds2lem  11946  opoe  12036  omoe  12037  opeo  12038  omeo  12039  gcddvds  12100  dfgcd2  12151  pcqmul  12441  xpsfrnel2  12929  eqgval  13293  txbasval  14435  cnmpt12  14455  cnmpt22  14462  2sqlem7  15208