Theorem syl6com 38

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 36	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
4	3	com12 33	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  1908  19.36imv  1968  sbequ2  2287  nfeqf2  2411  ax6e  2417  axc16i  2470  mo4  2596  rgen2a  3361  sbccomlem  3825  rspn0  4312  wefrc  5646  elinxp  6009  sorpssuni  7719  sorpssint  7720  ordzsl  7829  limuni3  7836  funcnvuni  7917  funrnex  7939  soxp  8113  frrlem4  8274  oaabs  8622  eceqoveq  8808  pssinf  9210  unbnn2  9245  inf0  9578  inf3lem5  9589  tcel  9700  frmin  9709  rankxpsuc  9842  carduni  9955  prdom2  9978  dfac5  10100  cflm  10221  indpi  10880  prlem934  11006  negf1o  11632  xrub  13329  injresinjlem  13810  hashgt12el  14449  hashgt12el2  14450  fi1uzind  14534  swrdwrdsymb  14690  cshwcsh2id  14855  cshwshash  17154  lidrididd  18718  dfgrp2  19019  symgextf1  19482  rngdi  20229  rngdir  20230  gsummoncoe1  22429  basis2  23069  fbdmn0  23952  rusgr1vtxlem  29846  upgrewlkle2  29865  clwwlknun  30372  conngrv2edg  30455  frcond1  30526  4cyclusnfrgr  30552  atcv0eq  32640  dfon2lem9  36152  altopthsn  36324  rankeq1o  36534  wl-orel12  38026  wl-equsb4  38072  rngoueqz  38451  hbtlem5  43717  ntrk0kbimka  44627  funressnfv  47635  afvco2  47768  ndmaovcl  47795  bgoldbtbndlem4  48428  isubgr3stgrlem4  48589  zlmodzxznm  49128