Theorem sylan9bb 714

Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.)

Hypotheses

Ref	Expression
sylan9bb.1	|- ( ph -> ( ps <-> ch ) )
sylan9bb.2	|- ( th -> ( ch <-> ta ) )

Assertion

Ref	Expression
sylan9bb	|- ( ( ph /\ th ) -> ( ps <-> ta ) )

Proof of Theorem sylan9bb

Step	Hyp	Ref	Expression
1		sylan9bb.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	adantr 472	. 2 |- ( ( ph /\ th ) -> ( ps <-> ch ) )
3		sylan9bb.2	. . 3 |- ( th -> ( ch <-> ta ) )
4	3	adantl 473	. 2 |- ( ( ph /\ th ) -> ( ch <-> ta ) )
5	2, 4	bitrd 261	1 |- ( ( ph /\ th ) -> ( ps <-> ta ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 376

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 190  df-an 378

This theorem is referenced by:  sylan9bbr  715  bi2anan9  890  baibd  923  rbaibd  924  syl3an9b  1363  nanbi12  1423  sbcom2  2294  2sb5rf  2300  2sb6rf  2301  eqeq12  2484  eleq12  2539  sbhypf  3081  ceqsrex2v  3162  sseq12  3441  2ralsng  3999  rexprg  4013  rextpg  4015  breq12  4400  reusv2lem5  4606  opelopabg  4719  brabg  4720  opelopab2  4722  ralxpf  4986  feq23  5723  f00  5778  fconstg  5783  f1oeq23  5821  f1o00  5861  fnelfp  6108  fnelnfp  6110  isofrlem  6249  f1oiso  6260  riota1a  6289  cbvmpt2x  6388  caovord  6499  caovord3  6501  f1oweALT  6796  oaordex  7277  oaass  7280  odi  7298  findcard2s  7830  unfilem1  7853  suppeqfsuppbi  7915  oieu  8072  r1pw  8334  carddomi2  8422  isacn  8493  cdadom2  8635  axdc2  8897  alephval2  9015  fpwwe2cbv  9073  fpwwe2lem2  9075  fpwwecbv  9087  fpwwelem  9088  canthwelem  9093  canthwe  9094  distrlem4pr  9469  axpre-sup  9611  nn0ind-raph  11058  elfz  11816  elfzp12  11899  expeq0  12340  leiso  12663  wrd2ind  12888  trcleq12lem  13132  dfrtrclrec2  13197  shftfib  13212  absdvdsb  14398  dvdsabsb  14399  unbenlem  14931  isprs  16253  isdrs  16257  pltval  16284  lublecllem  16312  istos  16359  isdlat  16517  znfld  19208  tgss2  20080  isopn2  20124  cnpf2  20343  lmbr  20351  isreg2  20470  fclsrest  21117  qustgplem  21213  ustuqtoplem  21332  xmetec  21527  nmogelb  21799  nmogelbOLD  21818  metdstri  21946  metdstriOLD  21961  tchcph  22289  ulmval  23414  iscgrg  24636  eupath2lem1  25784  eigrei  27568  eigorthi  27571  jplem1  28002  superpos  28088  chrelati  28098  br8d  28294  issiga  29007  eulerpartlemgvv  29282  br8  30467  br6  30468  br4  30469  brsegle  30946  topfne  31081  tailfb  31104  filnetlem1  31105  nndivsub  31188  bj-elequ12  31343  isbasisrelowllem1  31828  isbasisrelowllem2  31829  wl-2sb6d  31958  poimirlem26  32030  mblfinlem2  32042  cnambfre  32053  itgaddnclem2  32065  ftc1anclem1  32081  grpokerinj  32247  rngoisoval  32280  smprngopr  32349  ax12eq  32576  ax12el  32577  2llnjN  33203  2lplnj  33256  elpadd0  33445  lauteq  33731  lpolconN  35126  rexrabdioph  35708  eliunov2  36342  nzss  36736  iotasbc2  36841  xnn0xadd0  39238  istrlson  39902  ispthson  39934  isspthson  39935  eupth2lem1  40130  uhg0e  40196  cbvmpt2x2  40625