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  2257  nfeqf2  2382  ax6e  2388  axc16i  2441  mo4  2567  rgen2a  3342  sbccomlem  3820  rspn0  4309  wefrc  5619  elinxp  5979  sorpssuni  7679  sorpssint  7680  ordzsl  7789  limuni3  7796  funcnvuni  7876  funrnex  7900  soxp  8073  frrlem4  8233  oaabs  8578  eceqoveq  8763  pssinf  9166  unbnn2  9201  inf0  9534  inf3lem5  9545  tcel  9656  frmin  9665  rankxpsuc  9798  carduni  9897  prdom2  9920  dfac5  10043  cflm  10164  indpi  10822  prlem934  10948  negf1o  11571  xrub  13231  injresinjlem  13710  hashgt12el  14349  hashgt12el2  14350  fi1uzind  14434  swrdwrdsymb  14590  cshwcsh2id  14755  cshwshash  17036  lidrididd  18599  dfgrp2  18896  symgextf1  19354  rngdi  20099  rngdir  20100  gsummoncoe1  22256  basis2  22899  fbdmn0  23782  rusgr1vtxlem  29644  upgrewlkle2  29663  clwwlknun  30170  conngrv2edg  30253  frcond1  30324  4cyclusnfrgr  30350  atcv0eq  32437  dfon2lem9  35964  altopthsn  36136  rankeq1o  36346  bj-cbvalimt  36814  bj-cbveximt  36815  wl-orel12  37687  wl-equsb4  37733  rngoueqz  38112  hbtlem5  43406  ntrk0kbimka  44316  funressnfv  47325  afvco2  47458  ndmaovcl  47485  bgoldbtbndlem4  48090  isubgr3stgrlem4  48251  zlmodzxznm  48779