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  1882  sbequ2  2246  nfeqf2  2391  ax6e  2397  axc16i  2454  mo4  2646  rgen2a  3229  wefrc  5543  elinxp  5884  sorpssuni  7452  sorpssint  7453  ordzsl  7554  limuni3  7561  funcnvuni  7630  funrnex  7649  soxp  7817  wfrlem4  7952  wfrlem12  7960  oaabs  8265  eceqoveq  8396  php3  8697  pssinf  8722  unbnn2  8769  inf0  9078  inf3lem5  9089  tcel  9181  rankxpsuc  9305  carduni  9404  prdom2  9426  dfac5  9548  cflm  9666  indpi  10323  prlem934  10449  negf1o  11064  xrub  12699  injresinjlem  13151  hashgt12el  13777  hashgt12el2  13778  fi1uzind  13849  swrdwrdsymb  14018  cshwcsh2id  14184  cshwshash  16432  lidrididd  17874  dfgrp2  18122  symgextf1  18543  gsummoncoe1  20466  basis2  21553  fbdmn0  22436  rusgr1vtxlem  27363  upgrewlkle2  27382  clwwlknun  27885  conngrv2edg  27968  frcond1  28039  4cyclusnfrgr  28065  atcv0eq  30150  dfon2lem9  33031  trpredrec  33072  frmin  33079  frrlem4  33121  altopthsn  33417  rankeq1o  33627  bj-cbvalimt  33967  bj-cbveximt  33968  wl-orel12  34745  wl-equsb4  34787  rngoueqz  35212  hbtlem5  39721  ntrk0kbimka  40382  funressnfv  43272  afvco2  43369  ndmaovcl  43396  bgoldbtbndlem4  43967  rngdir  44147  zlmodzxznm  44546