Theorem bi2anan9 614

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 469	. 2 |- ( ph -> ( ( ps /\ ta ) <-> ( ch /\ ta ) ) )
3		bi2an9.2	. . 3 |- ( th -> ( ta <-> et ) )
4	3	anbi2d 468	. 2 |- ( th -> ( ( ch /\ ta ) <-> ( ch /\ et ) ) )
5	2, 4	sylan9bb 466	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  615  rspc2gv  2942  ralprg  3759  raltpg  3761  prssg  3870  prsspwg  3873  ssprss  3874  opelopab2a  4405  opelxp  4802  eqrel  4862  eqrelrel  4874  brcog  4945  dff13  5967  resoprab2  6178  ovig  6203  dfoprab4f  6420  f1o2ndf1  6457  eroveu  6893  th3qlem1  6904  th3qlem2  6905  th3q  6907  oviec  6908  endisj  7115  exmidapne  7619  dfplpq2  7714  dfmpq2  7715  ordpipqqs  7734  enq0enq  7791  mulnnnq0  7810  ltsrprg  8107  axcnre  8241  axmulgt0  8390  addltmul  9524  ltxr  10159  sumsqeq0  11036  ccat0  11345  mul0inf  11988  dvds2lem  12551  opoe  12643  omoe  12644  opeo  12645  omeo  12646  gcddvds  12721  dfgcd2  12772  pcqmul  13063  xpsfrnel2  13647  eqgval  14006  txbasval  15294  cnmpt12  15314  cnmpt22  15321  lgsquadlem3  16115  lgsquad  16116  2sqlem7  16157