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  1886  19.36imv  1946  sbequ2  2254  nfeqf2  2379  ax6e  2385  axc16i  2438  mo4  2563  rgen2a  3339  sbccomlem  3817  rspn0  4307  wefrc  5615  elinxp  5975  sorpssuni  7674  sorpssint  7675  ordzsl  7784  limuni3  7791  funcnvuni  7871  funrnex  7895  soxp  8068  frrlem4  8228  oaabs  8572  eceqoveq  8755  pssinf  9156  unbnn2  9191  inf0  9521  inf3lem5  9532  tcel  9643  frmin  9652  rankxpsuc  9785  carduni  9884  prdom2  9907  dfac5  10030  cflm  10151  indpi  10808  prlem934  10934  negf1o  11557  xrub  13221  injresinjlem  13700  hashgt12el  14339  hashgt12el2  14340  fi1uzind  14424  swrdwrdsymb  14580  cshwcsh2id  14745  cshwshash  17026  lidrididd  18588  dfgrp2  18885  symgextf1  19343  rngdi  20088  rngdir  20089  gsummoncoe1  22233  basis2  22876  fbdmn0  23759  rusgr1vtxlem  29577  upgrewlkle2  29596  clwwlknun  30103  conngrv2edg  30186  frcond1  30257  4cyclusnfrgr  30283  atcv0eq  32370  dfon2lem9  35844  altopthsn  36016  rankeq1o  36226  bj-cbvalimt  36694  bj-cbveximt  36695  wl-orel12  37566  wl-equsb4  37612  rngoueqz  37990  hbtlem5  43235  ntrk0kbimka  44146  funressnfv  47157  afvco2  47290  ndmaovcl  47317  bgoldbtbndlem4  47922  isubgr3stgrlem4  48083  zlmodzxznm  48612