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

Theorem sylan9bbr 681
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 680 . 2  |-  ( (
ph  /\  th )  ->  ( ps  <->  ta )
)
43ancoms 439 1  |-  ( ( th  /\  ph )  ->  ( ps  <->  ta )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  pm5.75  903  sbcom  2042  sbcom2  2066  2mo  2234  2eu6  2241  mpteq12f  4112  tfindsg  4667  findsg  4699  fconstfv  5750  f1oiso  5864  mpt2eq123  5923  dfoprab4f  6194  fmpt2x  6206  opiota  6306  oalimcl  6574  oeeui  6616  nnmword  6647  isinf  7092  elfi  7183  brwdomn0  7299  alephval3  7753  dfac2  7773  fin17  8036  isfin7-2  8038  ltmpi  8544  addclprlem1  8656  distrlem4pr  8666  1idpr  8669  qreccl  10352  0fz1  10829  xpnnenOLD  12504  dvdseq  12592  sscntz  14818  gexdvds  14911  cnprest  17033  txrest  17341  ptrescn  17349  flimrest  17694  txflf  17717  fclsrest  17735  tsmssubm  17841  mbfi1fseqlem4  19089  ubthlem1  21465  pjimai  22772  atcv1  22976  chirredi  22990  zmodid2  24025  axcontlem7  24670  trnij  25718  iepiclem  25926  raaan2  28056  sbcomwAUX7  29562  sbcomOLD7  29709  sbcom2OLD7  29715
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 177  df-an 360
  Copyright terms: Public domain W3C validator