Theorem sylan9bbr 543

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 542	. 2 |- ((ph /\ th) -> (ps <-> ta))
4	3	ancoms 438	1 |- ((th /\ ph) -> (ps <-> ta))

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

This theorem is referenced by:  bimsc1 752  sbcom 1260  sbcom2 1336  2mo 1450  2eu6 1457  otthg 2796  copsexg 2798  findsg 3163  tfindsg 3168  elrnopabg 3806  fconstfv 3855  f1oiso 3910  eloprabg 4013  elrnoprabg 4130  oalimcl 4200  nnaordex 4255  nnawordex 4256  aceq6b 4752  alephval3 4914  ltmpi 5043  addclprlem1 5130  distrlem4pr 5142  1idpr 5145  prlem936a 5165  ltxrt 5507  lt2msq 5883  nn1suc 5941  infmsup 6070  supxrre 6085  nn0ltp1let 6129  zaddclt 6167  qrecclt 6274  xpnnen 7500  znnen 7503  bastop 7641  islp2 7744  metxp 7831  atcv1t 10302  irred 10316  elo 10439  trnij 10608  cnvtr 10609

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