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  2377  ax6e  2383  axc16i  2436  mo4  2561  rgen2a  3368  rspn0  4353  wefrc  5671  elinxp  6020  sorpssuni  7722  sorpssint  7723  ordzsl  7834  limuni3  7841  funcnvuni  7922  funrnex  7940  soxp  8115  frrlem4  8274  wfrlem4OLD  8312  wfrlem12OLD  8320  oaabs  8647  eceqoveq  8816  php3OLD  9224  pssinf  9256  unbnn2  9300  inf0  9616  inf3lem5  9627  tcel  9740  frmin  9744  rankxpsuc  9877  carduni  9976  prdom2  10001  dfac5  10123  cflm  10245  indpi  10902  prlem934  11028  negf1o  11644  xrub  13291  injresinjlem  13752  hashgt12el  14382  hashgt12el2  14383  fi1uzind  14458  swrdwrdsymb  14612  cshwcsh2id  14779  cshwshash  17038  lidrididd  18589  dfgrp2  18847  symgextf1  19289  gsummoncoe1  21828  basis2  22454  fbdmn0  23338  rusgr1vtxlem  28844  upgrewlkle2  28863  clwwlknun  29365  conngrv2edg  29448  frcond1  29519  4cyclusnfrgr  29545  atcv0eq  31632  dfon2lem9  34763  altopthsn  34933  rankeq1o  35143  bj-cbvalimt  35516  bj-cbveximt  35517  wl-orel12  36380  wl-equsb4  36422  rngoueqz  36808  hbtlem5  41870  ntrk0kbimka  42790  funressnfv  45753  afvco2  45884  ndmaovcl  45911  bgoldbtbndlem4  46476  rngdi  46659  rngdir  46660  zlmodzxznm  47178