MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylan9bbr 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  2115  sbcom2  2140  2mo  2309  2eu6  2316  mpteq12f  4219  tfindsg  4773  findsg  4805  fconstfv  5886  f1oiso  6003  mpt2eq123  6065  dfoprab4f  6337  fmpt2x  6349  opiota  6464  oalimcl  6732  oeeui  6774  nnmword  6805  isinf  7251  elfi  7346  brwdomn0  7463  alephval3  7917  dfac2  7937  fin17  8200  isfin7-2  8202  ltmpi  8707  addclprlem1  8819  distrlem4pr  8829  1idpr  8832  qreccl  10519  0fz1  10999  hashle00  11589  xpnnenOLD  12729  dvdseq  12817  sscntz  15045  gexdvds  15138  cnprest  17268  txrest  17577  ptrescn  17585  flimrest  17929  txflf  17952  fclsrest  17970  tsmssubm  18086  mbfi1fseqlem4  19470  ubthlem1  22213  pjimai  23520  atcv1  23724  chirredi  23738  zmodid2  24886  axcontlem7  25616  raaan2  27614  sbcomwAUX7  28916  sbcomOLD7  29064  sbcom2OLD7  29070
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