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  1886  sbequ2  2250  nfeqf2  2395  ax6e  2401  axc16i  2458  mo4  2650  rgen2a  3229  wefrc  5549  elinxp  5890  sorpssuni  7458  sorpssint  7459  ordzsl  7560  limuni3  7567  funcnvuni  7636  funrnex  7655  soxp  7823  wfrlem4  7958  wfrlem12  7966  oaabs  8271  eceqoveq  8402  php3  8703  pssinf  8728  unbnn2  8775  inf0  9084  inf3lem5  9095  tcel  9187  rankxpsuc  9311  carduni  9410  prdom2  9432  dfac5  9554  cflm  9672  indpi  10329  prlem934  10455  negf1o  11070  xrub  12706  injresinjlem  13158  hashgt12el  13784  hashgt12el2  13785  fi1uzind  13856  swrdwrdsymb  14024  cshwcsh2id  14190  cshwshash  16438  lidrididd  17880  dfgrp2  18128  symgextf1  18549  gsummoncoe1  20472  basis2  21559  fbdmn0  22442  rusgr1vtxlem  27369  upgrewlkle2  27388  clwwlknun  27891  conngrv2edg  27974  frcond1  28045  4cyclusnfrgr  28071  atcv0eq  30156  dfon2lem9  33036  trpredrec  33077  frmin  33084  frrlem4  33126  altopthsn  33422  rankeq1o  33632  bj-cbvalimt  33972  bj-cbveximt  33973  wl-orel12  34766  wl-equsb4  34808  rngoueqz  35233  hbtlem5  39748  ntrk0kbimka  40409  funressnfv  43298  afvco2  43395  ndmaovcl  43422  bgoldbtbndlem4  43993  rngdir  44173  zlmodzxznm  44572