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  3345  sbccomlem  3832  rspn0  4319  wefrc  5632  elinxp  5990  sorpssuni  7708  sorpssint  7709  ordzsl  7821  limuni3  7828  funcnvuni  7908  funrnex  7932  soxp  8108  frrlem4  8268  oaabs  8612  eceqoveq  8795  pssinf  9203  unbnn2  9244  inf0  9574  inf3lem5  9585  tcel  9698  frmin  9702  rankxpsuc  9835  carduni  9934  prdom2  9959  dfac5  10082  cflm  10203  indpi  10860  prlem934  10986  negf1o  11608  xrub  13272  injresinjlem  13748  hashgt12el  14387  hashgt12el2  14388  fi1uzind  14472  swrdwrdsymb  14627  cshwcsh2id  14794  cshwshash  17075  lidrididd  18597  dfgrp2  18894  symgextf1  19351  rngdi  20069  rngdir  20070  gsummoncoe1  22195  basis2  22838  fbdmn0  23721  rusgr1vtxlem  29515  upgrewlkle2  29534  clwwlknun  30041  conngrv2edg  30124  frcond1  30195  4cyclusnfrgr  30221  atcv0eq  32308  dfon2lem9  35779  altopthsn  35949  rankeq1o  36159  bj-cbvalimt  36627  bj-cbveximt  36628  wl-orel12  37499  wl-equsb4  37545  rngoueqz  37934  hbtlem5  43117  ntrk0kbimka  44028  funressnfv  47044  afvco2  47177  ndmaovcl  47204  bgoldbtbndlem4  47809  isubgr3stgrlem4  47968  zlmodzxznm  48486