Theorem bi2anan9 843

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 685	. 2 |- (ph -> ((ps /\ ta) <-> (ch /\ ta)))
3		bi2an9.2	. . 3 |- (th -> (ta <-> et))
4	3	anbi2d 684	. 2 |- (th -> ((ch /\ ta) <-> (ch /\ et)))
5	2, 4	sylan9bb 680	1 |- ((ph /\ th) -> ((ps /\ ta) <-> (ch /\ et)))

Syntax hints:   -> wi 4   <-> wb 176   /\ wa 358

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  bi2anan9r  844  2mo  2282  2eu6  2289  2reu5  3044  ralprg  3775  raltpg  3777  prssg  3862  ssofeq  4077  ncfinraise  4481  ncfinlower  4483  nnpweq  4523  opelopab2a  4702  brsi  4761  dfxp2  5113  fvopab4t  5385  dff13  5471  resoprab2  5582  ovig  5597  brtxp  5783  fnpprod  5843  fundmen  6043  endisj  6051  mucnc  6131  peano4nc  6150  ce0addcnnul  6179  ce0nnulb  6182  ceclb  6183  ceclr  6187  sbth  6206  dflec2  6210  letc  6231  addcdi  6250  fnfrec  6320