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-mp 5  ax-1 6  ax-2 7  ax-3 8

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

This theorem is referenced by:  bi2anan9r  844  2mo  2282  2eu6  2289  2reu5  3045  ralprg  3776  raltpg  3778  prssg  3863  ssofeq  4078  ncfinraise  4482  ncfinlower  4484  nnpweq  4524  opelopab2a  4703  brsi  4762  dfxp2  5114  fvopab4t  5386  dff13  5472  resoprab2  5583  ovig  5598  brtxp  5784  fnpprod  5844  fundmen  6044  endisj  6052  mucnc  6132  peano4nc  6151  ce0addcnnul  6180  ce0nnulb  6183  ceclb  6184  ceclr  6188  sbth  6207  dflec2  6211  letc  6232  addcdi  6251  fnfrec  6321