Theorem sylan9bbr 600

Description: Nested syllogism inference conjoining dissimilar antecedents.

Hypotheses

Ref	Expression
sylan9bbr.1	|- (ph -> (ps <-> ch))
sylan9bbr.2	|- (th -> (ch <-> ta))

Assertion

Ref	Expression
sylan9bbr	|- ((th /\ ph) -> (ps <-> ta))

Proof of Theorem sylan9bbr

Step	Hyp	Ref	Expression
1		sylan9bbr.1	. . 3 |- (ph -> (ps <-> ch))
2		sylan9bbr.2	. . 3 |- (th -> (ch <-> ta))
3	1, 2	sylan9bb 599	. 2 |- ((ph /\ th) -> (ps <-> ta))
4	3	ancoms 484	1 |- ((th /\ ph) -> (ps <-> ta))

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

This theorem is referenced by:  bimsc1 823  sbcom 1632  sbcom2 1724  2mo 1851  2eu6 1858  otthg 3535  copsexgOLD 3538  tfindsg 3944  findsg 3980  elrnopabg 4773  fconstfv 4825  f1oiso 4881  eloprabg 4936  elrnoprabg 5066  oalimcl 5242  nnaordex 5306  nnawordex 5307  infenomsub 5889  aceq6b 5904  alephval3 6051  ltmpi 6183  addclprlem1 6270  distrlem4pr 6282  1idpr 6285  prlem936a 6305  ltxr 6664  lt2msqi 7064  nn1suc 7122  infmsup 7277  supxrre 7292  nn0ltp1le 7336  zaddcl 7374  qreccl 7453  xpnnen 8768  znnen 8771  bastop1 8912  islp2 9023  metxp 9111  atcv1 11952  irredi 11966  zmodid2 13614  elo 14342  trnij 15015  cnvtr 15016  iepiclem 15172  infenomsubOLD 15398

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