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  2880  ralprg  3673  raltpg  3675  prssg  3779  prsspwg  3782  opelopab2a  4299  opelxp  4693  eqrel  4752  eqrelrel  4764  brcog  4833  dff13  5815  resoprab2  6019  ovig  6044  dfoprab4f  6251  f1o2ndf1  6286  eroveu  6685  th3qlem1  6696  th3qlem2  6697  th3q  6699  oviec  6700  endisj  6883  exmidapne  7327  dfplpq2  7421  dfmpq2  7422  ordpipqqs  7441  enq0enq  7498  mulnnnq0  7517  ltsrprg  7814  axcnre  7948  axmulgt0  8098  addltmul  9228  ltxr  9850  sumsqeq0  10710  mul0inf  11406  dvds2lem  11968  opoe  12060  omoe  12061  opeo  12062  omeo  12063  gcddvds  12130  dfgcd2  12181  pcqmul  12472  xpsfrnel2  12989  eqgval  13353  txbasval  14503  cnmpt12  14523  cnmpt22  14530  lgsquadlem3  15320  lgsquad  15321  2sqlem7  15362