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 4444  mapdom2 4492  unfilem1 4543  carduni 4850  alephval2 4894  axrepndlem2 4937  distrlem4pr 5122  lt2msq 5869  nn0ltp1let 6115  zltp1let 6169  nn0ind-raph 6202  qsqueeze 6266  seq1suclem 6302  snunioolem 6400  elfzt 6457  expeq0t 6571  clm3 7064  elcncf 7250  znnen 7487  unbenlem 7489  iscld2 7655  isopn2 7658  qdensere 7736  cncnp2 7764  metcnpf 7868  metcnf 7869  lmbr 7913  iscauf 7924  lmss 7938  lmclimnn 7949  metcn4 7956  nvcnf 8312  nvcnpf 8313  spwpr2 8643  eigre 9745  eigorth 9748  elnlfnt 9837  jplem1 10180  superpos 10266  chrelat 10276  nndivsub 10406  elo 10428

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