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  1889  19.36imv  1949  sbequ2  2242  nfeqf2  2378  ax6e  2384  axc16i  2437  mo4  2567  rgen2a  3159  rspn0  4287  wefrc  5584  elinxp  5932  sorpssuni  7594  sorpssint  7595  ordzsl  7701  limuni3  7708  funcnvuni  7787  funrnex  7805  soxp  7979  frrlem4  8114  wfrlem4OLD  8152  wfrlem12OLD  8160  oaabs  8487  eceqoveq  8620  php3OLD  9016  pssinf  9042  unbnn2  9080  inf0  9388  inf3lem5  9399  tcel  9512  frmin  9516  rankxpsuc  9649  carduni  9748  prdom2  9771  dfac5  9893  cflm  10015  indpi  10672  prlem934  10798  negf1o  11414  xrub  13055  injresinjlem  13516  hashgt12el  14146  hashgt12el2  14147  fi1uzind  14220  swrdwrdsymb  14384  cshwcsh2id  14550  cshwshash  16815  lidrididd  18363  dfgrp2  18613  symgextf1  19038  gsummoncoe1  21484  basis2  22110  fbdmn0  22994  rusgr1vtxlem  27963  upgrewlkle2  27982  clwwlknun  28485  conngrv2edg  28568  frcond1  28639  4cyclusnfrgr  28665  atcv0eq  30750  dfon2lem9  33776  altopthsn  34272  rankeq1o  34482  bj-cbvalimt  34829  bj-cbveximt  34830  wl-orel12  35679  wl-equsb4  35721  rngoueqz  36107  hbtlem5  40960  ntrk0kbimka  41656  funressnfv  44548  afvco2  44679  ndmaovcl  44706  bgoldbtbndlem4  45271  rngdir  45451  zlmodzxznm  45849