Theorem sylan9bb 599

Description: Nested syllogism inference conjoining dissimilar antecedents.

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

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240

This theorem is referenced by:  sylan9bbr 600  bi2anan9 694  syl3an9b 1166  sbcom 1632  sbcom2 1724  ax11eq 1754  ax11el 1755  eqeq12 1896  eleq12 1959  ceqsrex2v 2395  moi2 2435  moi 2436  sbhypf 2452  sseq12 2640  breq12 3343  opelopabsbOLD 3565  opelopabg 3567  opelopabf 3572  ralxpf 4043  feq23 4554  f00 4601  fconstg 4604  f1o00 4668  isofrlem 4878  f1oiso 4881  f1oweALT 4883  oprabval2gf 4955  ndmoprg 4976  caoprcom 4986  caoprord 4989  caoprord3 4991  sbcopeq1a 5051  reiota1 5108  oaordex 5240  oaass 5243  odi 5258  pw2en 5505  mapdom2 5588  unfilem1 5641  ordtype 5691  carduni 6010  alephval2 6050  axrepndlem2 6097  distrlem4pr 6282  addcani 6505  lt2msqi 7064  nn0ltp1le 7336  zltp1le 7390  nn0ind-raph 7426  qsqueeze 7461  snunioolem 7583  elfz 7641  seq1suclem 7729  expeq0 7828  clm3i 8339  elcncf 8527  znnen 8771  unbenlem 8773  iscld2 8946  isopn2 8949  qdensere 9027  cncnp2 9056  metcnpf 9161  metcnf 9162  lmbr 9206  iscauf 9217  lmss 9231  lmclimnn 9242  metcn4 9249  isga2 9452  nvcnf 9659  nvcnpf 9660  spwpr2 10001  txcn 10227  stoig 10251  hausfillim 10303  eigrei 11397  eigorthi 11400  elnlfn 11489  jplem1 11840  superpos 11926  chrelati 11936  nndivsub 14258  elo 14342  limfilnei 14943  iepiclem 15172  issubcatb 15195  subtr2 15353  fictblem 15370  fictb 15371  ordtypeOLD 15382  2ndcctbss 15478  topbasfne 15499  neibastop2lem1 15519  neibastop2lem4 15522  ufileu 15573  tailfb 15639  elfzp12 15795  tlmbr 15904  grpkerinj 16042  smprngpr 16200  erdisj3 16266  prter3 16286  iotasbc2 16384  pltval 16781  pgeval 16794  lubid 16807  elpadd0 17270

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 164  df-an 242

Copyright terms: Public domain