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  2382  ax6e  2388  axc16i  2441  mo4  2566  rgen2a  3355  sbccomlem  3849  rspn0  4336  wefrc  5653  elinxp  6011  sorpssuni  7731  sorpssint  7732  ordzsl  7845  limuni3  7852  funcnvuni  7933  funrnex  7957  soxp  8133  frrlem4  8293  wfrlem4OLD  8331  wfrlem12OLD  8339  oaabs  8665  eceqoveq  8841  php3OLD  9238  pssinf  9269  unbnn2  9310  inf0  9640  inf3lem5  9651  tcel  9764  frmin  9768  rankxpsuc  9901  carduni  10000  prdom2  10025  dfac5  10148  cflm  10269  indpi  10926  prlem934  11052  negf1o  11672  xrub  13333  injresinjlem  13808  hashgt12el  14445  hashgt12el2  14446  fi1uzind  14530  swrdwrdsymb  14685  cshwcsh2id  14852  cshwshash  17129  lidrididd  18653  dfgrp2  18950  symgextf1  19407  rngdi  20125  rngdir  20126  gsummoncoe1  22251  basis2  22894  fbdmn0  23777  rusgr1vtxlem  29572  upgrewlkle2  29591  clwwlknun  30098  conngrv2edg  30181  frcond1  30252  4cyclusnfrgr  30278  atcv0eq  32365  dfon2lem9  35814  altopthsn  35984  rankeq1o  36194  bj-cbvalimt  36662  bj-cbveximt  36663  wl-orel12  37534  wl-equsb4  37580  rngoueqz  37969  hbtlem5  43127  ntrk0kbimka  44038  funressnfv  47052  afvco2  47185  ndmaovcl  47212  bgoldbtbndlem4  47802  isubgr3stgrlem4  47961  zlmodzxznm  48453