Theorem sylan9bb 705

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  706  bi2anan9  882  baibd  918  rbaibd  919  syl3an9b  1334  nanbi12  1394  sbcom2  2241  2sb5rf  2247  2sb6rf  2248  eqeq12  2442  eleq12  2499  sbhypf  3129  ceqsrex2v  3208  sseq12  3488  2ralsng  4034  rexprg  4048  rextpg  4050  breq12  4426  reusv2lem5  4627  opelopabg  4736  brabg  4737  opelopab2  4739  ralxpf  4998  feq23  5729  f00  5780  fconstg  5785  f1oeq23  5823  f1o00  5861  fnelfp  6105  fnelnfp  6107  isofrlem  6244  f1oiso  6255  riota1a  6284  cbvmpt2x  6381  caovord  6492  caovord3  6494  f1oweALT  6789  oaordex  7265  oaass  7268  odi  7286  findcard2s  7816  unfilem1  7839  suppeqfsuppbi  7901  oieu  8058  r1pw  8319  carddomi2  8407  isacn  8477  cdadom2  8619  axdc2  8881  alephval2  8999  fpwwe2cbv  9057  fpwwe2lem2  9059  fpwwecbv  9071  fpwwelem  9072  canthwelem  9077  canthwe  9078  distrlem4pr  9453  axpre-sup  9595  nn0ind-raph  11037  elfz  11792  elfzp12  11875  expeq0  12303  leiso  12621  wrd2ind  12830  trcleq12lem  13051  dfrtrclrec2  13114  shftfib  13129  absdvdsb  14314  dvdsabsb  14315  unbenlem  14845  isprs  16168  isdrs  16172  pltval  16199  lublecllem  16227  istos  16274  isdlat  16432  znfld  19123  tgss2  19995  isopn2  20039  cnpf2  20258  lmbr  20266  isreg2  20385  fclsrest  21031  qustgplem  21127  ustuqtoplem  21246  xmetec  21441  nmogelb  21713  nmogelbOLD  21732  metdstri  21860  metdstriOLD  21875  tchcph  22203  ulmval  23327  iscgrg  24549  eupath2lem1  25697  eigrei  27479  eigorthi  27482  jplem1  27913  superpos  27999  chrelati  28009  br8d  28214  issiga  28935  eulerpartlemgvv  29211  br8  30397  br6  30398  br4  30399  brsegle  30874  topfne  31009  tailfb  31032  filnetlem1  31033  nndivsub  31116  bj-elequ12  31233  isbasisrelowllem1  31716  isbasisrelowllem2  31717  wl-2sb6d  31846  poimirlem26  31924  mblfinlem2  31936  cnambfre  31947  itgaddnclem2  31959  ftc1anclem1  31975  grpokerinj  32141  rngoisoval  32174  smprngopr  32243  ax12eq  32475  ax12el  32476  2llnjN  33095  2lplnj  33148  elpadd0  33337  lauteq  33623  lpolconN  35018  rexrabdioph  35600  eliunov2  36175  nzss  36568  iotasbc2  36673  uhgr0e  38870  uhg0e  39030  cbvmpt2x2  39461