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  1883  19.36imv  1943  sbequ2  2247  nfeqf2  2380  ax6e  2386  axc16i  2439  mo4  2564  rgen2a  3369  sbccomlem  3878  rspn0  4362  wefrc  5683  elinxp  6039  sorpssuni  7751  sorpssint  7752  ordzsl  7866  limuni3  7873  funcnvuni  7955  funrnex  7977  soxp  8153  frrlem4  8313  wfrlem4OLD  8351  wfrlem12OLD  8359  oaabs  8685  eceqoveq  8861  php3OLD  9259  pssinf  9290  unbnn2  9331  inf0  9659  inf3lem5  9670  tcel  9783  frmin  9787  rankxpsuc  9920  carduni  10019  prdom2  10044  dfac5  10167  cflm  10288  indpi  10945  prlem934  11071  negf1o  11691  xrub  13351  injresinjlem  13823  hashgt12el  14458  hashgt12el2  14459  fi1uzind  14543  swrdwrdsymb  14697  cshwcsh2id  14864  cshwshash  17139  lidrididd  18696  dfgrp2  18993  symgextf1  19454  rngdi  20178  rngdir  20179  gsummoncoe1  22328  basis2  22974  fbdmn0  23858  rusgr1vtxlem  29620  upgrewlkle2  29639  clwwlknun  30141  conngrv2edg  30224  frcond1  30295  4cyclusnfrgr  30321  atcv0eq  32408  dfon2lem9  35773  altopthsn  35943  rankeq1o  36153  bj-cbvalimt  36622  bj-cbveximt  36623  wl-orel12  37492  wl-equsb4  37538  rngoueqz  37927  hbtlem5  43117  ntrk0kbimka  44029  funressnfv  46993  afvco2  47126  ndmaovcl  47153  bgoldbtbndlem4  47733  isubgr3stgrlem4  47872  zlmodzxznm  48343