Theorem syl6com 37

Description: Syllogism inference with commuted antecedents. (Contributed by NM, 25-May-2005.)

Hypotheses

Ref	Expression
syl6com.1	⊢ (𝜑 → (𝜓 → 𝜒))
syl6com.2	⊢ (𝜒 → 𝜃)

Assertion

Ref	Expression
syl6com	⊢ (𝜓 → (𝜑 → 𝜃))

Proof of Theorem syl6com

Step	Hyp	Ref	Expression
1		syl6com.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2		syl6com.2	. . 3 ⊢ (𝜒 → 𝜃)
3	1, 2	syl6 35	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
4	3	com12 32	1 ⊢ (𝜓 → (𝜑 → 𝜃))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  19.33b  1887  19.36imv  1947  sbequ2  2257  nfeqf2  2382  ax6e  2388  axc16i  2441  mo4  2567  rgen2a  3334  sbccomlem  3808  rspn0  4297  wefrc  5616  elinxp  5976  sorpssuni  7677  sorpssint  7678  ordzsl  7787  limuni3  7794  funcnvuni  7874  funrnex  7898  soxp  8070  frrlem4  8230  oaabs  8575  eceqoveq  8760  pssinf  9163  unbnn2  9198  inf0  9531  inf3lem5  9542  tcel  9653  frmin  9662  rankxpsuc  9795  carduni  9894  prdom2  9917  dfac5  10040  cflm  10161  indpi  10819  prlem934  10945  negf1o  11569  xrub  13253  injresinjlem  13734  hashgt12el  14373  hashgt12el2  14374  fi1uzind  14458  swrdwrdsymb  14614  cshwcsh2id  14779  cshwshash  17064  lidrididd  18627  dfgrp2  18927  symgextf1  19385  rngdi  20130  rngdir  20131  gsummoncoe1  22282  basis2  22925  fbdmn0  23808  rusgr1vtxlem  29676  upgrewlkle2  29695  clwwlknun  30202  conngrv2edg  30285  frcond1  30356  4cyclusnfrgr  30382  atcv0eq  32470  dfon2lem9  35992  altopthsn  36164  rankeq1o  36374  wl-orel12  37847  wl-equsb4  37893  rngoueqz  38272  hbtlem5  43571  ntrk0kbimka  44481  funressnfv  47488  afvco2  47621  ndmaovcl  47648  bgoldbtbndlem4  48281  isubgr3stgrlem4  48442  zlmodzxznm  48970