HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem bi2anan9 631
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
StepHypRef Expression
1 bi2an9.1 . . 3 |- (ph -> (ps <-> ch))
21anbi1d 616 . 2 |- (ph -> ((ps /\ ta) <-> (ch /\ ta)))
3 bi2an9.2 . . 3 |- (th -> (ta <-> et))
43anbi2d 615 . 2 |- (th -> ((ch /\ ta) <-> (ch /\ et)))
52, 4sylan9bb 539 1 |- ((ph /\ th) -> ((ps /\ ta) <-> (ch /\ et)))
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223
This theorem is referenced by:  bi2anan9r 632  2mo 1445  2eu6 1452  copsex4g 2789  eqrel 3245  feq23 3615  f1fv 3865  oprabval4g 4022  om00el 4197  th3qlem1 4304  th3qlem2 4305  oprec 4308  unen 4420  endisj 4423  aceq5lem4 4718  ordpipq 5036  genpv 5082  genpprecl 5084  distrlem5pr 5111  ltsrpr 5166  axcnre 5266  axmulgt0 5486  lt2msq 5837  acdc3 7437  acdc2 7440  acdc5 7443  acdc 7445  ruclem12 7472  bra11 9979  leopaddt 10003  cmpbva 10396
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