Theorem bi2anan9 630

Description: Deduction joining two equivalences to form equivalence of conjunctions.

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

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223

This theorem is referenced by:  bi2anan9r 631  2mo 1440  2eu6 1447  copsex4g 2784  eqrel 3240  feq23 3609  f1fv 3859  oprabval4g 4016  om00el 4191  th3qlem1 4298  th3qlem2 4299  oprec 4302  unen 4414  endisj 4417  aceq5lem4 4710  ordpipq 5028  genpv 5074  genpprecl 5076  distrlem5pr 5103  ltsrpr 5158  axcnre 5258  axmulgt0 5478  lt2msq 5829  acdc3 7429  acdc2 7432  acdc5 7435  acdc 7437  ruclem12 7464  bra11 9954  leopaddt 9977  cmpbva 10360

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

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain