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  2935  ralprg  3742  raltpg  3744  prssg  3853  prsspwg  3856  ssprss  3857  opelopab2a  4385  opelxp  4781  eqrel  4841  eqrelrel  4853  brcog  4924  dff13  5943  resoprab2  6152  ovig  6177  dfoprab4f  6389  f1o2ndf1  6426  eroveu  6862  th3qlem1  6873  th3qlem2  6874  th3q  6876  oviec  6877  endisj  7077  exmidapne  7576  dfplpq2  7671  dfmpq2  7672  ordpipqqs  7691  enq0enq  7748  mulnnnq0  7767  ltsrprg  8064  axcnre  8198  axmulgt0  8347  addltmul  9477  ltxr  10111  sumsqeq0  10984  ccat0  11288  mul0inf  11930  dvds2lem  12493  opoe  12585  omoe  12586  opeo  12587  omeo  12588  gcddvds  12663  dfgcd2  12714  pcqmul  13005  xpsfrnel2  13576  eqgval  13957  txbasval  15149  cnmpt12  15169  cnmpt22  15176  lgsquadlem3  15969  lgsquad  15970  2sqlem7  16011