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 ⊢ (𝜓 → (𝜑 → 𝜃))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  19.33b  1914  19.36imv  1974  sbequ2  2284  nfeqf2  2408  ax6e  2414  axc16i  2467  mo4  2593  rgen2a  3359  sbccomlem  3821  rspn0  4310  wefrc  5654  elinxp  6017  sorpssuni  7731  sorpssint  7732  ordzsl  7839  limuni3  7846  funcnvuni  7927  funrnex  7949  soxp  8123  frrlem4  8284  oaabs  8632  eceqoveq  8818  pssinf  9220  unbnn2  9255  inf0  9588  inf3lem5  9599  tcel  9710  frmin  9719  rankxpsuc  9852  carduni  9974  prdom2  9997  dfac5  10119  cflm  10239  indpi  10898  prlem934  11024  negf1o  11650  xrub  13344  injresinjlem  13826  hashgt12el  14466  hashgt12el2  14467  fi1uzind  14551  swrdwrdsymb  14707  cshwcsh2id  14872  cshwshash  17170  lidrididd  18734  dfgrp2  19035  symgextf1  19497  rngdi  20244  rngdir  20245  gsummoncoe1  22479  basis2  23119  fbdmn0  24002  rusgr1vtxlem  29948  upgrewlkle2  29967  clwwlknun  30474  conngrv2edg  30557  frcond1  30628  4cyclusnfrgr  30654  atcv0eq  32742  dfon2lem9  36289  altopthsn  36461  rankeq1o  36671  wl-orel12  38194  wl-equsb4  38240  rngoueqz  38619  hbtlem5  43883  ntrk0kbimka  44793  funressnfv  47808  afvco2  47941  ndmaovcl  47968  bgoldbtbndlem4  48601  isubgr3stgrlem4  48762  zlmodzxznm  49305