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  1885  19.36imv  1945  sbequ2  2250  nfeqf2  2375  ax6e  2381  axc16i  2434  mo4  2559  rgen2a  3336  sbccomlem  3823  rspn0  4309  wefrc  5617  elinxp  5974  sorpssuni  7672  sorpssint  7673  ordzsl  7785  limuni3  7792  funcnvuni  7872  funrnex  7896  soxp  8069  frrlem4  8229  oaabs  8573  eceqoveq  8756  pssinf  9161  unbnn2  9202  inf0  9536  inf3lem5  9547  tcel  9660  frmin  9664  rankxpsuc  9797  carduni  9896  prdom2  9919  dfac5  10042  cflm  10163  indpi  10820  prlem934  10946  negf1o  11568  xrub  13232  injresinjlem  13708  hashgt12el  14347  hashgt12el2  14348  fi1uzind  14432  swrdwrdsymb  14587  cshwcsh2id  14753  cshwshash  17034  lidrididd  18562  dfgrp2  18859  symgextf1  19318  rngdi  20063  rngdir  20064  gsummoncoe1  22211  basis2  22854  fbdmn0  23737  rusgr1vtxlem  29551  upgrewlkle2  29570  clwwlknun  30074  conngrv2edg  30157  frcond1  30228  4cyclusnfrgr  30254  atcv0eq  32341  dfon2lem9  35764  altopthsn  35934  rankeq1o  36144  bj-cbvalimt  36612  bj-cbveximt  36613  wl-orel12  37484  wl-equsb4  37530  rngoueqz  37919  hbtlem5  43101  ntrk0kbimka  44012  funressnfv  47028  afvco2  47161  ndmaovcl  47188  bgoldbtbndlem4  47793  isubgr3stgrlem4  47952  zlmodzxznm  48470