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  2029  sbcom2  2053  2mo  2221  2eu6  2228  mpteq12f  4096  tfindsg  4651  findsg  4683  fconstfv  5734  f1oiso  5848  mpt2eq123  5907  dfoprab4f  6178  fmpt2x  6190  opiota  6290  oalimcl  6558  oeeui  6600  nnmword  6631  isinf  7076  elfi  7167  brwdomn0  7283  alephval3  7737  dfac2  7757  fin17  8020  isfin7-2  8022  ltmpi  8528  addclprlem1  8640  distrlem4pr  8650  1idpr  8653  qreccl  10336  0fz1  10813  xpnnenOLD  12488  dvdseq  12576  sscntz  14802  gexdvds  14895  cnprest  17017  txrest  17325  ptrescn  17333  flimrest  17678  txflf  17701  fclsrest  17719  tsmssubm  17825  mbfi1fseqlem4  19073  ubthlem1  21449  pjimai  22756  atcv1  22960  chirredi  22974  zmodid2  24010  axcontlem7  24598  trnij  25615  iepiclem  25823  raaan2  27953
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