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  2251  nfeqf2  2376  ax6e  2382  axc16i  2435  mo4  2560  rgen2a  3335  sbccomlem  3818  rspn0  4304  wefrc  5608  elinxp  5965  sorpssuni  7660  sorpssint  7661  ordzsl  7770  limuni3  7777  funcnvuni  7857  funrnex  7881  soxp  8054  frrlem4  8214  oaabs  8558  eceqoveq  8741  pssinf  9141  unbnn2  9176  inf0  9506  inf3lem5  9517  tcel  9630  frmin  9634  rankxpsuc  9767  carduni  9866  prdom2  9889  dfac5  10012  cflm  10133  indpi  10790  prlem934  10916  negf1o  11539  xrub  13203  injresinjlem  13682  hashgt12el  14321  hashgt12el2  14322  fi1uzind  14406  swrdwrdsymb  14562  cshwcsh2id  14727  cshwshash  17008  lidrididd  18570  dfgrp2  18867  symgextf1  19326  rngdi  20071  rngdir  20072  gsummoncoe1  22216  basis2  22859  fbdmn0  23742  rusgr1vtxlem  29559  upgrewlkle2  29578  clwwlknun  30082  conngrv2edg  30165  frcond1  30236  4cyclusnfrgr  30262  atcv0eq  32349  dfon2lem9  35804  altopthsn  35974  rankeq1o  36184  bj-cbvalimt  36652  bj-cbveximt  36653  wl-orel12  37524  wl-equsb4  37570  rngoueqz  37959  hbtlem5  43140  ntrk0kbimka  44051  funressnfv  47053  afvco2  47186  ndmaovcl  47213  bgoldbtbndlem4  47818  isubgr3stgrlem4  47979  zlmodzxznm  48508