Theorem bi2anan9 538

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

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  bi2anan9r  539  ralprg  3412  raltpg  3414  prssg  3512  prsspwg  3514  opelopab2a  3993  opelxp  4317  eqrel  4372  eqrelrel  4384  brcog  4445  dff13  5350  resoprab2  5540  ovig  5564  dfoprab4f  5761  f1o2ndf1  5791  eroveu  6133  th3qlem1  6144  th3qlem2  6145  th3q  6147  oviec  6148  endisj  6234  dfplpq2  6338  dfmpq2  6339  ordpipqqs  6358  enq0enq  6414  mulnnnq0  6433  ltsrprg  6675  axcnre  6765  axmulgt0  6888  addltmul  7938  ltxr  8465  sumsqeq0  8985