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  2240  nfeqf2  2375  ax6e  2381  axc16i  2434  mo4  2564  rgen2a  3340  rspn0  4300  wefrc  5615  elinxp  5962  sorpssuni  7648  sorpssint  7649  ordzsl  7760  limuni3  7767  funcnvuni  7847  funrnex  7865  soxp  8038  frrlem4  8176  wfrlem4OLD  8214  wfrlem12OLD  8222  oaabs  8550  eceqoveq  8683  php3OLD  9090  pssinf  9122  unbnn2  9166  inf0  9479  inf3lem5  9490  tcel  9603  frmin  9607  rankxpsuc  9740  carduni  9839  prdom2  9864  dfac5  9986  cflm  10108  indpi  10765  prlem934  10891  negf1o  11507  xrub  13148  injresinjlem  13609  hashgt12el  14238  hashgt12el2  14239  fi1uzind  14312  swrdwrdsymb  14474  cshwcsh2id  14641  cshwshash  16904  lidrididd  18452  dfgrp2  18701  symgextf1  19126  gsummoncoe1  21582  basis2  22208  fbdmn0  23092  rusgr1vtxlem  28244  upgrewlkle2  28263  clwwlknun  28765  conngrv2edg  28848  frcond1  28919  4cyclusnfrgr  28945  atcv0eq  31030  dfon2lem9  34052  altopthsn  34402  rankeq1o  34612  bj-cbvalimt  34959  bj-cbveximt  34960  wl-orel12  35826  wl-equsb4  35868  rngoueqz  36254  hbtlem5  41267  ntrk0kbimka  42022  funressnfv  44955  afvco2  45086  ndmaovcl  45113  bgoldbtbndlem4  45678  rngdir  45858  zlmodzxznm  46256