Theorem sylan9bbr 539

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

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

This theorem is referenced by:  bimsc1 748  sbcom 1253  sbcom2 1329  2mo 1440  2eu6 1447  otthg 2780  copsexg 2782  findsg 3147  tfindsg 3152  elrnopabg 3785  fconstfv 3834  f1oiso 3889  eloprabg 3992  elrnoprabg 4108  oalimcl 4178  nnaordex 4233  nnawordex 4234  aceq6b 4714  alephval3 4875  ltmpi 5003  addclprlem1 5090  distrlem4pr 5102  1idpr 5105  prlem936a 5125  ltxrt 5467  lt2msq 5829  nn1suc 5887  infmsup 6015  supxrre 6030  nn0ltp1let 6074  zaddclt 6112  qrecclt 6211  xpnnen 7441  znnen 7445  bastop 7584  islp2 7688  metxp 7774  atcv1t 10215  irred 10229  elo 10345  trnij 10481  cnvtr 10482

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