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  1913  19.36imv  1973  sbequ2  2283  nfeqf2  2407  ax6e  2413  axc16i  2466  mo4  2592  rgen2a  3358  sbccomlem  3821  rspn0  4310  wefrc  5655  elinxp  6018  sorpssuni  7729  sorpssint  7730  ordzsl  7840  limuni3  7847  funcnvuni  7928  funrnex  7950  soxp  8124  frrlem4  8285  oaabs  8633  eceqoveq  8819  pssinf  9221  unbnn2  9256  inf0  9589  inf3lem5  9600  tcel  9711  frmin  9720  rankxpsuc  9853  carduni  9966  prdom2  9989  dfac5  10111  cflm  10232  indpi  10891  prlem934  11017  negf1o  11643  xrub  13337  injresinjlem  13819  hashgt12el  14459  hashgt12el2  14460  fi1uzind  14544  swrdwrdsymb  14700  cshwcsh2id  14865  cshwshash  17163  lidrididd  18727  dfgrp2  19028  symgextf1  19490  rngdi  20237  rngdir  20238  gsummoncoe1  22447  basis2  23087  fbdmn0  23970  rusgr1vtxlem  29903  upgrewlkle2  29922  clwwlknun  30429  conngrv2edg  30512  frcond1  30583  4cyclusnfrgr  30609  atcv0eq  32697  dfon2lem9  36247  altopthsn  36419  rankeq1o  36629  wl-orel12  38132  wl-equsb4  38178  rngoueqz  38557  hbtlem5  43825  ntrk0kbimka  44735  funressnfv  47747  afvco2  47880  ndmaovcl  47907  bgoldbtbndlem4  48540  isubgr3stgrlem4  48701  zlmodzxznm  49244