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  2376  ax6e  2382  axc16i  2435  mo4  2560  rgen2a  3347  sbccomlem  3835  rspn0  4322  wefrc  5635  elinxp  5993  sorpssuni  7711  sorpssint  7712  ordzsl  7824  limuni3  7831  funcnvuni  7911  funrnex  7935  soxp  8111  frrlem4  8271  oaabs  8615  eceqoveq  8798  pssinf  9210  unbnn2  9251  inf0  9581  inf3lem5  9592  tcel  9705  frmin  9709  rankxpsuc  9842  carduni  9941  prdom2  9966  dfac5  10089  cflm  10210  indpi  10867  prlem934  10993  negf1o  11615  xrub  13279  injresinjlem  13755  hashgt12el  14394  hashgt12el2  14395  fi1uzind  14479  swrdwrdsymb  14634  cshwcsh2id  14801  cshwshash  17082  lidrididd  18604  dfgrp2  18901  symgextf1  19358  rngdi  20076  rngdir  20077  gsummoncoe1  22202  basis2  22845  fbdmn0  23728  rusgr1vtxlem  29522  upgrewlkle2  29541  clwwlknun  30048  conngrv2edg  30131  frcond1  30202  4cyclusnfrgr  30228  atcv0eq  32315  dfon2lem9  35786  altopthsn  35956  rankeq1o  36166  bj-cbvalimt  36634  bj-cbveximt  36635  wl-orel12  37506  wl-equsb4  37552  rngoueqz  37941  hbtlem5  43124  ntrk0kbimka  44035  funressnfv  47048  afvco2  47181  ndmaovcl  47208  bgoldbtbndlem4  47813  isubgr3stgrlem4  47972  zlmodzxznm  48490