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

Theorem syl2and 608
Description: A syllogism deduction. (Contributed by NM, 15-Dec-2004.)
Hypotheses
Ref Expression
syl2and.1 (𝜑 → (𝜓𝜒))
syl2and.2 (𝜑 → (𝜃𝜏))
syl2and.3 (𝜑 → ((𝜒𝜏) → 𝜂))
Assertion
Ref Expression
syl2and (𝜑 → ((𝜓𝜃) → 𝜂))

Proof of Theorem syl2and
StepHypRef Expression
1 syl2and.1 . 2 (𝜑 → (𝜓𝜒))
2 syl2and.2 . . 3 (𝜑 → (𝜃𝜏))
3 syl2and.3 . . 3 (𝜑 → ((𝜒𝜏) → 𝜂))
42, 3sylan2d 605 . 2 (𝜑 → ((𝜒𝜃) → 𝜂))
51, 4syland 603 1 (𝜑 → ((𝜓𝜃) → 𝜂))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  anim12d  609  ax7  2015  dffi3  9471  cflim2  10303  axpre-sup  11209  xle2add  13301  fzen  13581  rpmulgcd2  16693  pcqmul  16891  sbcie2s  17198  initoeu1  18056  termoeu1  18063  plttr  18387  pospo  18390  lublecllem  18405  latjlej12  18500  latmlem12  18516  hausnei2  23361  uncmp  23411  itgsubst  26090  mpodvdsmulf1o  27237  dvdsmulf1o  27239  2sqlem8a  27469  precsexlem10  28240  axcontlem9  28987  uspgr2wlkeq  29664  shintcli  31348  cvntr  32311  cdj3i  32460  f1resrcmplf1dlem  35100  satffunlem  35406  bj-bary1  37313  heicant  37662  itg2addnc  37681  dihmeetlem1N  41292  modelaxreplem1  44995  fmtnofac2lem  47555  2itscp  48702  mofsn  48753
  Copyright terms: Public domain W3C validator