Theorem bi2anan9 885

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

Syntax hints:   -> wi 4   <-> wb 188   /\ wa 371

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 189  df-an 373

This theorem is referenced by:  bi2anan9r  886  2reu5  3250  ralprg  4023  raltpg  4025  prssg  4130  prsspwg  4132  opelopab2a  4719  opelxp  4867  eqrel  4927  eqrelrel  4939  brcog  5004  tpres  6122  dff13  6164  resoprab2  6398  ovig  6423  dfoprab4f  6856  f1o2ndf1  6909  om00el  7282  oeoe  7305  eroveu  7463  endisj  7664  infxpen  8450  dfac5lem4  8562  sornom  8712  ltsrpr  9506  axcnre  9593  axmulgt0  9713  wloglei  10153  mulge0b  10482  addltmul  10855  ltxr  11422  sumsqeq0  12360  rlim  13571  cpnnen  14293  dvds2lem  14327  gcddvds  14489  opoe  14773  omoe  14774  opeo  14775  omeo  14776  pcqmul  14815  xpsfrnel2  15483  eqgval  16878  frgpuplem  17434  mpfind  18771  2ndcctbss  20482  txbasval  20633  cnmpt12  20694  cnmpt22  20701  prdsxmslem2  21556  ishtpy  22015  bcthlem1  22304  bcth  22309  volun  22510  vitali  22583  itg1addlem3  22668  rolle  22954  mumullem2  24119  lgsquadlem3  24296  lgsquad  24297  2sqlem7  24310  axpasch  24983  usgra2adedgwlkonALT  25356  usgra2wlkspthlem1  25359  el2wlkonotot1  25614  frg2wot1  25797  frg2woteqm  25799  numclwwlkovg  25827  hlimi  26853  leopadd  27797  eqrelrd2  28234  isinftm  28510  metidv  28707  altopthg  30746  altopthbg  30747  brsegle  30887  finxpreclem3  31797  itg2addnclem3  32007  fzadd2  32082  prtlem13  32452  dib1dim  34745  pellex  35691  ssprss  39011  wlkson  39666