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  1884  19.36imv  1944  sbequ2  2248  nfeqf2  2381  ax6e  2387  axc16i  2440  mo4  2565  rgen2a  3370  sbccomlem  3868  rspn0  4355  wefrc  5678  elinxp  6036  sorpssuni  7753  sorpssint  7754  ordzsl  7867  limuni3  7874  funcnvuni  7955  funrnex  7979  soxp  8155  frrlem4  8315  wfrlem4OLD  8353  wfrlem12OLD  8361  oaabs  8687  eceqoveq  8863  php3OLD  9262  pssinf  9293  unbnn2  9334  inf0  9662  inf3lem5  9673  tcel  9786  frmin  9790  rankxpsuc  9923  carduni  10022  prdom2  10047  dfac5  10170  cflm  10291  indpi  10948  prlem934  11074  negf1o  11694  xrub  13355  injresinjlem  13827  hashgt12el  14462  hashgt12el2  14463  fi1uzind  14547  swrdwrdsymb  14701  cshwcsh2id  14868  cshwshash  17143  lidrididd  18684  dfgrp2  18981  symgextf1  19440  rngdi  20158  rngdir  20159  gsummoncoe1  22313  basis2  22959  fbdmn0  23843  rusgr1vtxlem  29606  upgrewlkle2  29625  clwwlknun  30132  conngrv2edg  30215  frcond1  30286  4cyclusnfrgr  30312  atcv0eq  32399  dfon2lem9  35793  altopthsn  35963  rankeq1o  36173  bj-cbvalimt  36641  bj-cbveximt  36642  wl-orel12  37513  wl-equsb4  37559  rngoueqz  37948  hbtlem5  43145  ntrk0kbimka  44057  funressnfv  47060  afvco2  47193  ndmaovcl  47220  bgoldbtbndlem4  47800  isubgr3stgrlem4  47941  zlmodzxznm  48419