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  1918  19.36imv  1978  sbequ2  2284  nfeqf2  2406  ax6e  2412  axc16i  2465  mo4  2591  rgen2a  3356  sbccomlem  3816  rspn0  4303  wefrc  5641  elinxp  6006  sorpssuni  7731  sorpssint  7732  ordzsl  7839  limuni3  7846  funcnvuni  7927  funrnex  7949  soxp  8124  frrlem4  8285  oaabs  8635  eceqoveq  8821  pssinf  9231  unbnn2  9267  inf0  9600  inf3lem5  9611  tcel  9722  frmin  9731  rankxpsuc  9872  carduni  10034  prdom2  10057  dfac5  10179  cflm  10299  indpi  10964  prlem934  11090  negf1o  11716  xrub  13412  injresinjlem  13894  hashgt12el  14535  hashgt12el2  14536  fi1uzind  14620  swrdwrdsymb  14780  cshwcsh2id  14947  cshwshash  17244  lidrididd  18813  dfgrp2  19135  symgextf1  19597  rngdi  20344  rngdir  20345  gsummoncoe1  22588  basis2  23231  fbdmn0  24115  rusgr1vtxlem  30102  upgrewlkle2  30121  clwwlknun  30637  conngrv2edg  30730  frcond1  30801  4cyclusnfrgr  30827  atcv0eq  32915  dfon2lem9  36475  altopthsn  36648  rankeq1o  36854  mh-inf3f1  37251  wl-orel12  38363  wl-equsb4  38409  rngoueqz  38794  hbtlem5  44073  ntrk0kbimka  44983  funressnfv  48035  afvco2  48168  ndmaovcl  48195  bgoldbtbndlem4  48828  isubgr3stgrlem4  48989  zlmodzxznm  49531