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  2923  ralprg  3724  raltpg  3726  prssg  3835  prsspwg  3838  ssprss  3839  opelopab2a  4365  opelxp  4761  eqrel  4821  eqrelrel  4833  brcog  4903  dff13  5919  resoprab2  6128  ovig  6153  dfoprab4f  6365  f1o2ndf1  6402  eroveu  6838  th3qlem1  6849  th3qlem2  6850  th3q  6852  oviec  6853  endisj  7051  exmidapne  7539  dfplpq2  7634  dfmpq2  7635  ordpipqqs  7654  enq0enq  7711  mulnnnq0  7730  ltsrprg  8027  axcnre  8161  axmulgt0  8310  addltmul  9440  ltxr  10071  sumsqeq0  10943  ccat0  11239  mul0inf  11881  dvds2lem  12444  opoe  12536  omoe  12537  opeo  12538  omeo  12539  gcddvds  12614  dfgcd2  12665  pcqmul  12956  xpsfrnel2  13509  eqgval  13890  txbasval  15078  cnmpt12  15098  cnmpt22  15105  lgsquadlem3  15898  lgsquad  15899  2sqlem7  15940