Theorem sylan9bb 538

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

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

This theorem is referenced by:  sylan9bbr 539  bi2anan9 630  syl3an9b 888  sbcom 1253  sbcom2 1329  ax11eq 1356  ax11el 1357  eqeq12 1479  eleq12 1528  ceqsrex2v 1881  moi 1915  sbhypf 1929  sbhyp 1930  sseq12 2074  breq12 2614  opabsb 2804  opelopabg 2806  ralxpf 3210  f00 3642  fconstg 3644  f1o00 3699  isofrlem 3886  f1oiso 3889  f1oweALT 3891  oprabval2gf 4011  ndmoprg 4028  caoprcom 4039  caoprord 4042  caoprord3 4044  sbcopeq1a 4095  oaordex 4176  oaass 4179  odi 4194  pw2en 4426  mapdom2 4474  unfilem1 4524  carduni 4830  alephval2 4874  axrepndlem2 4917  distrlem4pr 5102  lt2msq 5829  nn0ltp1let 6074  zltp1let 6128  nn0ind-raph 6162  qsqueeze 6218  seq1suclem 6253  snunioolem 6347  elfzt 6403  expeq0t 6517  clm3 7017  elcncf 7200  znnen 7445  unbenlem 7447  iscld2 7612  isopn2 7615  qdensere 7691  cncnp2 7718  metcnpf 7822  metcnf 7823  lmbr 7866  iscauf 7877  lmss 7888  lmclimnn 7899  metcn4 7905  nvcnf 8265  eigre 9677  eigorth 9680  elnlfnt 9768  jplem1 10105  superpos 10189  chrelat 10199  elo 10345

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