Theorem sylan9bb 540

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 528	1 |- ((ph /\ th) -> (ps <-> ta))

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

This theorem is referenced by:  sylan9bbr 541  bi2anan9 632  syl3an9b 891  sbcom 1258  sbcom2 1334  ax11eq 1363  ax11el 1364  eqeq12 1487  eleq12 1536  ceqsrex2v 1890  moi2 1924  moi 1925  sbhypf 1939  sbhyp 1940  sseq12 2084  breq12 2624  opabsb 2815  opelopabg 2817  ralxpf 3220  f00 3657  fconstg 3659  f1o00 3714  isofrlem 3901  f1oiso 3904  f1oweALT 3906  oprabval2gf 4026  ndmoprg 4043  caoprcom 4053  caoprord 4056  caoprord3 4058  sbcopeq1a 4111  oaordex 4192  oaass 4195  odi 4210  pw2en 4446  mapdom2 4494  unfilem1 4548  carduni 4858  alephval2 4902  axrepndlem2 4945  distrlem4pr 5130  lt2msq 5881  nn0ltp1let 6127  zltp1let 6181  nn0ind-raph 6214  qsqueeze 6280  seq1suclem 6316  snunioolem 6414  elfzt 6471  expeq0t 6585  clm3 7079  elcncf 7265  znnen 7502  unbenlem 7504  iscld2 7670  isopn2 7673  qdensere 7751  cncnp2 7779  metcnpf 7883  metcnf 7884  lmbr 7928  iscauf 7939  lmss 7953  lmclimnn 7964  metcn4 7971  nvcnf 8327  nvcnpf 8328  spwpr2 8658  eigre 9760  eigorth 9763  elnlfnt 9852  jplem1 10195  superpos 10281  chrelat 10291  nndivsub 10421  elo 10444

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