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  3343  sbccomlem  3821  rspn0  4310  wefrc  5626  elinxp  5986  sorpssuni  7687  sorpssint  7688  ordzsl  7797  limuni3  7804  funcnvuni  7884  funrnex  7908  soxp  8081  frrlem4  8241  oaabs  8586  eceqoveq  8771  pssinf  9174  unbnn2  9209  inf0  9542  inf3lem5  9553  tcel  9664  frmin  9673  rankxpsuc  9806  carduni  9905  prdom2  9928  dfac5  10051  cflm  10172  indpi  10830  prlem934  10956  negf1o  11579  xrub  13239  injresinjlem  13718  hashgt12el  14357  hashgt12el2  14358  fi1uzind  14442  swrdwrdsymb  14598  cshwcsh2id  14763  cshwshash  17044  lidrididd  18607  dfgrp2  18904  symgextf1  19362  rngdi  20107  rngdir  20108  gsummoncoe1  22264  basis2  22907  fbdmn0  23790  rusgr1vtxlem  29673  upgrewlkle2  29692  clwwlknun  30199  conngrv2edg  30282  frcond1  30353  4cyclusnfrgr  30379  atcv0eq  32466  dfon2lem9  36002  altopthsn  36174  rankeq1o  36384  bj-cbvalimt  36868  bj-cbveximt  36869  wl-orel12  37755  wl-equsb4  37801  rngoueqz  38180  hbtlem5  43474  ntrk0kbimka  44384  funressnfv  47392  afvco2  47525  ndmaovcl  47552  bgoldbtbndlem4  48157  isubgr3stgrlem4  48318  zlmodzxznm  48846