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  1892  19.36imv  1952  sbequ2  2261  nfeqf2  2385  ax6e  2391  axc16i  2444  mo4  2570  rgen2a  3336  sbccomlem  3808  rspn0  4291  wefrc  5619  elinxp  5978  sorpssuni  7682  sorpssint  7683  ordzsl  7792  limuni3  7799  funcnvuni  7879  funrnex  7903  soxp  8076  frrlem4  8236  oaabs  8581  eceqoveq  8766  pssinf  9169  unbnn2  9204  inf0  9540  inf3lem5  9551  tcel  9662  frmin  9671  rankxpsuc  9804  carduni  9903  prdom2  9926  dfac5  10049  cflm  10170  indpi  10828  prlem934  10954  negf1o  11578  xrub  13262  injresinjlem  13743  hashgt12el  14382  hashgt12el2  14383  fi1uzind  14467  swrdwrdsymb  14623  cshwcsh2id  14788  cshwshash  17073  lidrididd  18636  dfgrp2  18936  symgextf1  19394  rngdi  20139  rngdir  20140  gsummoncoe1  22301  basis2  22941  fbdmn0  23824  rusgr1vtxlem  29681  upgrewlkle2  29700  clwwlknun  30207  conngrv2edg  30290  frcond1  30361  4cyclusnfrgr  30387  atcv0eq  32475  dfon2lem9  36018  altopthsn  36190  rankeq1o  36400  wl-orel12  37883  wl-equsb4  37929  rngoueqz  38308  hbtlem5  43574  ntrk0kbimka  44484  funressnfv  47507  afvco2  47640  ndmaovcl  47667  bgoldbtbndlem4  48300  isubgr3stgrlem4  48461  zlmodzxznm  48989