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  28875  upgrewlkle2  28894  clwwlknun  29396  conngrv2edg  29479  frcond1  29550  4cyclusnfrgr  29576  atcv0eq  31663  dfon2lem9  34794  altopthsn  34964  rankeq1o  35174  bj-cbvalimt  35564  bj-cbveximt  35565  wl-orel12  36428  wl-equsb4  36470  rngoueqz  36856  hbtlem5  41918  ntrk0kbimka  42838  funressnfv  45801  afvco2  45932  ndmaovcl  45959  bgoldbtbndlem4  46524  rngdi  46707  rngdir  46708  zlmodzxznm  47226