Theorem bi2anan9 632

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

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

This theorem is referenced by:  bi2anan9r 633  2mo 1447  2eu6 1454  copsex4g 2794  eqrel 3250  feq23 3623  f1fv 3874  oprabval4g 4031  om00el 4207  th3qlem1 4314  th3qlem2 4315  oprec 4318  unen 4434  endisj 4437  aceq5lem4 4738  ordpipq 5056  genpv 5102  genpprecl 5104  distrlem5pr 5131  ltsrpr 5186  axcnre 5286  axmulgt0 5506  lt2msq 5881  acdc3 7487  acdc2 7490  acdc5 7493  acdc 7495  ruclem12 7521  spwpr2 8658  bra11 10041  leopaddt 10065  cmpbva 10464  rcfpfillem4 10591  rcfpfillem4OLD 10592

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