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  5909  resoprab2  6118  ovig  6143  dfoprab4f  6356  f1o2ndf1  6393  eroveu  6795  th3qlem1  6806  th3qlem2  6807  th3q  6809  oviec  6810  endisj  7008  exmidapne  7479  dfplpq2  7574  dfmpq2  7575  ordpipqqs  7594  enq0enq  7651  mulnnnq0  7670  ltsrprg  7967  axcnre  8101  axmulgt0  8251  addltmul  9381  ltxr  10010  sumsqeq0  10880  ccat0  11173  mul0inf  11802  dvds2lem  12365  opoe  12457  omoe  12458  opeo  12459  omeo  12460  gcddvds  12535  dfgcd2  12586  pcqmul  12877  xpsfrnel2  13430  eqgval  13811  txbasval  14993  cnmpt12  15013  cnmpt22  15020  lgsquadlem3  15810  lgsquad  15811  2sqlem7  15852