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

Theorem syld3an2 1365
Description: A syllogism inference. (Contributed by NM, 20-May-2007.)
Hypotheses
Ref Expression
syld3an2.1 ((𝜑𝜒𝜃) → 𝜓)
syld3an2.2 ((𝜑𝜓𝜃) → 𝜏)
Assertion
Ref Expression
syld3an2 ((𝜑𝜒𝜃) → 𝜏)

Proof of Theorem syld3an2
StepHypRef Expression
1 syld3an2.1 . . . 4 ((𝜑𝜒𝜃) → 𝜓)
213com23 1263 . . 3 ((𝜑𝜃𝜒) → 𝜓)
3 syld3an2.2 . . . 4 ((𝜑𝜓𝜃) → 𝜏)
433com23 1263 . . 3 ((𝜑𝜃𝜓) → 𝜏)
52, 4syld3an3 1363 . 2 ((𝜑𝜃𝜒) → 𝜏)
653com23 1263 1 ((𝜑𝜒𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1031
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 196  df-an 385  df-3an 1033
This theorem is referenced by:  nppcan2  10191  nnncan  10195  nnncan2  10197  ltdivmul  10777  ledivmul  10778  ltdiv23  10793  lediv23  10794  xrmaxlt  11886  xrltmin  11887  xrmaxle  11888  xrlemin  11889  swrdtrcfv  13293  dvdssub2  14861  dvdsgcdb  15100  lcmdvdsb  15164  vdwapun  15516  poslubdg  16972  ipodrsfi  16986  mulginvcom  17388  matinvgcell  20060  mdetrsca2  20229  mdetrlin2  20232  mdetunilem5  20241  decpmatmul  20396  islp3  20760  bddibl  23412  nvpi  26906  nvabs  26911  nmmulg  29340  subdivcomb2  30865  lineid  31360  oplecon1b  33506  opltcon1b  33510  oldmm2  33523  oldmj2  33527  cmt3N  33556  2llnneN  33713  cvrexchlem  33723  pmod2iN  34153  polcon2N  34223  paddatclN  34253  osumcllem3N  34262  ltrnval1  34438  cdleme48fv  34805  cdlemg33b  35013  trlcolem  35032  cdlemh  35123  cdlemi1  35124  cdlemi2  35125  cdlemi  35126  cdlemk4  35140  cdlemk19u1  35275  cdlemn3  35504  hgmapfval  36196  pell14qrgap  36457  stoweidlem22  38915  stoweidlem26  38919  sigarexp  39697  pfxtrcfv  40264  pfxco  40301  lindszr  42052
  Copyright terms: Public domain W3C validator