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  1884  19.36imv  1944  sbequ2  2250  nfeqf2  2385  ax6e  2391  axc16i  2444  mo4  2569  rgen2a  3379  sbccomlem  3891  rspn0  4379  wefrc  5694  elinxp  6048  sorpssuni  7767  sorpssint  7768  ordzsl  7882  limuni3  7889  funcnvuni  7972  funrnex  7994  soxp  8170  frrlem4  8330  wfrlem4OLD  8368  wfrlem12OLD  8376  oaabs  8704  eceqoveq  8880  php3OLD  9287  pssinf  9319  unbnn2  9361  inf0  9690  inf3lem5  9701  tcel  9814  frmin  9818  rankxpsuc  9951  carduni  10050  prdom2  10075  dfac5  10198  cflm  10319  indpi  10976  prlem934  11102  negf1o  11720  xrub  13374  injresinjlem  13837  hashgt12el  14471  hashgt12el2  14472  fi1uzind  14556  swrdwrdsymb  14710  cshwcsh2id  14877  cshwshash  17152  lidrididd  18708  dfgrp2  19002  symgextf1  19463  rngdi  20187  rngdir  20188  gsummoncoe1  22333  basis2  22979  fbdmn0  23863  rusgr1vtxlem  29623  upgrewlkle2  29642  clwwlknun  30144  conngrv2edg  30227  frcond1  30298  4cyclusnfrgr  30324  atcv0eq  32411  dfon2lem9  35755  altopthsn  35925  rankeq1o  36135  bj-cbvalimt  36605  bj-cbveximt  36606  wl-orel12  37465  wl-equsb4  37511  rngoueqz  37900  hbtlem5  43085  ntrk0kbimka  44001  funressnfv  46958  afvco2  47091  ndmaovcl  47118  bgoldbtbndlem4  47682  zlmodzxznm  48226