Theorem sylan9bb 707

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 467	. 2 |- ( ( ph /\ th ) -> ( ps <-> ch ) )
3		sylan9bb.2	. . 3 |- ( th -> ( ch <-> ta ) )
4	3	adantl 468	. 2 |- ( ( ph /\ th ) -> ( ch <-> ta ) )
5	2, 4	bitrd 257	1 |- ( ( ph /\ th ) -> ( ps <-> ta ) )

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:  sylan9bbr  708  bi2anan9  885  baibd  921  rbaibd  922  syl3an9b  1339  nanbi12  1400  sbcom2  2276  2sb5rf  2282  2sb6rf  2283  eqeq12  2466  eleq12  2521  sbhypf  3097  ceqsrex2v  3176  sseq12  3457  2ralsng  4010  rexprg  4024  rextpg  4026  breq12  4410  reusv2lem5  4611  opelopabg  4722  brabg  4723  opelopab2  4725  ralxpf  4984  feq23  5718  f00  5770  fconstg  5775  f1oeq23  5813  f1o00  5852  fnelfp  6097  fnelnfp  6099  isofrlem  6236  f1oiso  6247  riota1a  6276  cbvmpt2x  6374  caovord  6485  caovord3  6487  f1oweALT  6782  oaordex  7264  oaass  7267  odi  7285  findcard2s  7817  unfilem1  7840  suppeqfsuppbi  7902  oieu  8059  r1pw  8321  carddomi2  8409  isacn  8480  cdadom2  8622  axdc2  8884  alephval2  9002  fpwwe2cbv  9060  fpwwe2lem2  9062  fpwwecbv  9074  fpwwelem  9075  canthwelem  9080  canthwe  9081  distrlem4pr  9456  axpre-sup  9598  nn0ind-raph  11042  elfz  11797  elfzp12  11880  expeq0  12309  leiso  12629  wrd2ind  12841  trcleq12lem  13069  dfrtrclrec2  13132  shftfib  13147  absdvdsb  14333  dvdsabsb  14334  unbenlem  14864  isprs  16187  isdrs  16191  pltval  16218  lublecllem  16246  istos  16293  isdlat  16451  znfld  19143  tgss2  20015  isopn2  20059  cnpf2  20278  lmbr  20286  isreg2  20405  fclsrest  21051  qustgplem  21147  ustuqtoplem  21266  xmetec  21461  nmogelb  21733  nmogelbOLD  21752  metdstri  21880  metdstriOLD  21895  tchcph  22223  ulmval  23347  iscgrg  24569  eupath2lem1  25717  eigrei  27499  eigorthi  27502  jplem1  27933  superpos  28019  chrelati  28029  br8d  28230  issiga  28945  eulerpartlemgvv  29221  br8  30408  br6  30409  br4  30410  brsegle  30887  topfne  31022  tailfb  31045  filnetlem1  31046  nndivsub  31129  bj-elequ12  31289  isbasisrelowllem1  31770  isbasisrelowllem2  31771  wl-2sb6d  31900  poimirlem26  31978  mblfinlem2  31990  cnambfre  32001  itgaddnclem2  32013  ftc1anclem1  32029  grpokerinj  32195  rngoisoval  32228  smprngopr  32297  ax12eq  32524  ax12el  32525  2llnjN  33144  2lplnj  33197  elpadd0  33386  lauteq  33672  lpolconN  35067  rexrabdioph  35649  eliunov2  36283  nzss  36677  iotasbc2  36782  xnn0xadd0  39098  iswlkOn  39667  istrlson  39685  ispthson  39710  isspthson  39711  uhg0e  39792  cbvmpt2x2  40221