Theorem sylan9bb 539

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

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223

This theorem is referenced by:  sylan9bbr 540  bi2anan9 631  syl3an9b 889  sbcom 1256  sbcom2 1332  ax11eq 1361  ax11el 1362  eqeq12 1484  eleq12 1533  ceqsrex2v 1886  moi2 1920  moi 1921  sbhypf 1935  sbhyp 1936  sseq12 2080  breq12 2619  opabsb 2810  opelopabg 2812  ralxpf 3215  f00 3648  fconstg 3650  f1o00 3705  isofrlem 3892  f1oiso 3895  f1oweALT 3897  oprabval2gf 4017  ndmoprg 4034  caoprcom 4045  caoprord 4048  caoprord3 4050  sbcopeq1a 4101  oaordex 4182  oaass 4185  odi 4200  pw2en 4432  mapdom2 4480  unfilem1 4530  carduni 4838  alephval2 4882  axrepndlem2 4925  distrlem4pr 5110  lt2msq 5837  nn0ltp1let 6082  zltp1let 6136  nn0ind-raph 6170  qsqueeze 6226  seq1suclem 6261  snunioolem 6355  elfzt 6411  expeq0t 6525  clm3 7025  elcncf 7208  znnen 7453  unbenlem 7455  iscld2 7620  isopn2 7623  qdensere 7701  cncnp2 7729  metcnpf 7835  metcnf 7836  lmbr 7880  iscauf 7891  lmss 7904  lmclimnn 7915  metcn4 7921  nvcnf 8278  eigre 9700  eigorth 9703  elnlfnt 9791  jplem1 10133  superpos 10218  chrelat 10228  nndivsub 10357  elo 10381

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 147  df-an 225

Copyright terms: Public domain