MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylan9bbr Structured version   Unicode version

Theorem sylan9bbr 682
Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.)
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
StepHypRef Expression
1 sylan9bbr.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
2 sylan9bbr.2 . . 3  |-  ( th 
->  ( ch  <->  ta )
)
31, 2sylan9bb 681 . 2  |-  ( (
ph  /\  th )  ->  ( ps  <->  ta )
)
43ancoms 440 1  |-  ( ( th  /\  ph )  ->  ( ps  <->  ta )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  pm5.75  904  sbcom  2164  sbcom2  2189  2mo  2358  2eu6  2365  mpteq12f  4277  tfindsg  4832  findsg  4864  fconstfv  5946  f1oiso  6063  mpt2eq123  6125  dfoprab4f  6397  fmpt2x  6409  opiota  6527  oalimcl  6795  oeeui  6837  nnmword  6868  isinf  7314  elfi  7410  brwdomn0  7529  alephval3  7983  dfac2  8003  fin17  8266  isfin7-2  8268  ltmpi  8773  addclprlem1  8885  distrlem4pr  8895  1idpr  8898  qreccl  10586  0fz1  11066  hashle00  11661  xpnnenOLD  12801  dvdseq  12889  sscntz  15117  gexdvds  15210  cnprest  17345  txrest  17655  ptrescn  17663  flimrest  18007  txflf  18030  fclsrest  18048  tsmssubm  18164  mbfi1fseqlem4  19602  ubthlem1  22364  pjimai  23671  atcv1  23875  chirredi  23889  zmodid2  25106  axcontlem7  25901  raaan2  27910  hashfirdm  28133  hashfzdm  28134  sbcomwAUX7  29515  sbcom2NEW7  29571  sbcomOLD7  29682
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator