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  5625  elinxp  5985  sorpssuni  7686  sorpssint  7687  ordzsl  7796  limuni3  7803  funcnvuni  7883  funrnex  7907  soxp  8079  frrlem4  8239  oaabs  8584  eceqoveq  8769  pssinf  9172  unbnn2  9207  inf0  9542  inf3lem5  9553  tcel  9664  frmin  9673  rankxpsuc  9806  carduni  9905  prdom2  9928  dfac5  10051  cflm  10172  indpi  10830  prlem934  10956  negf1o  11580  xrub  13264  injresinjlem  13745  hashgt12el  14384  hashgt12el2  14385  fi1uzind  14469  swrdwrdsymb  14625  cshwcsh2id  14790  cshwshash  17075  lidrididd  18638  dfgrp2  18938  symgextf1  19396  rngdi  20141  rngdir  20142  gsummoncoe1  22273  basis2  22916  fbdmn0  23799  rusgr1vtxlem  29656  upgrewlkle2  29675  clwwlknun  30182  conngrv2edg  30265  frcond1  30336  4cyclusnfrgr  30362  atcv0eq  32450  dfon2lem9  35971  altopthsn  36143  rankeq1o  36353  wl-orel12  37836  wl-equsb4  37882  rngoueqz  38261  hbtlem5  43556  ntrk0kbimka  44466  funressnfv  47485  afvco2  47618  ndmaovcl  47645  bgoldbtbndlem4  48278  isubgr3stgrlem4  48439  zlmodzxznm  48967