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

Theorem sylan9bbr 736
Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.)
Hypotheses
Ref Expression
sylan9bbr.1 (𝜑 → (𝜓𝜒))
sylan9bbr.2 (𝜃 → (𝜒𝜏))
Assertion
Ref Expression
sylan9bbr ((𝜃𝜑) → (𝜓𝜏))

Proof of Theorem sylan9bbr
StepHypRef Expression
1 sylan9bbr.1 . . 3 (𝜑 → (𝜓𝜒))
2 sylan9bbr.2 . . 3 (𝜃 → (𝜒𝜏))
31, 2sylan9bb 735 . 2 ((𝜑𝜃) → (𝜓𝜏))
43ancoms 469 1 ((𝜃𝜑) → (𝜓𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197  df-an 386
This theorem is referenced by:  pm5.75  977  pm5.75OLD  978  sbcom2  2443  sbal1  2458  sbal2  2459  mpteq12f  4722  otthg  4944  fmptsng  6419  f1oiso  6586  mpt2eq123  6699  elovmpt2rab  6865  elovmpt2rab1  6866  ovmpt3rabdm  6877  elovmpt3rab1  6878  tfindsg  7045  findsg  7078  dfoprab4f  7211  opiota  7214  fmpt2x  7221  oalimcl  7625  oeeui  7667  nnmword  7698  isinf  8158  elfi  8304  brwdomn0  8459  alephval3  8918  dfac2  8938  fin17  9201  isfin7-2  9203  ltmpi  9711  addclprlem1  9823  distrlem4pr  9833  1idpr  9836  qreccl  11793  0fz1  12346  zmodid2  12681  ccatrcl1  13359  eqwrds3  13685  divgcdcoprm0  15360  sscntz  17740  gexdvds  17980  cnprest  21074  txrest  21415  ptrescn  21423  flimrest  21768  txflf  21791  fclsrest  21809  tsmssubm  21927  mbfi1fseqlem4  23466  axcontlem7  25831  uhgreq12g  25941  nbuhgr2vtx1edgb  26229  wlkcomp  26507  uhgrwkspthlem2  26631  clwlkcomp  26656  hashecclwwlksn1  26934  umgrhashecclwwlk  26935  numclwlk1lem2fo  27199  ubthlem1  27696  pjimai  29005  atcv1  29209  chirredi  29223  bj-restsn  33010  wl-sbcom2d-lem1  33313  wl-sbalnae  33316  ptrest  33379  poimirlem28  33408  heicant  33415  ftc1anclem1  33456  sbeqi  33939  ralbi12f  33940  iineq12f  33944  nzss  38336  raaan2  40938  rngcinv  41746  rngcinvALTV  41758  ringcinv  41797  ringcinvALTV  41821  snlindsntorlem  42024
  Copyright terms: Public domain W3C validator