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  1932  nfeqf2  2338  ax6e  2346  axc16i  2401  rgen2a  3158  wefrc  5349  elinxp  5683  elresOLD  5685  sorpssuni  7223  sorpssint  7224  ordzsl  7323  limuni3  7330  funcnvuni  7398  funrnex  7412  soxp  7571  wfrlem4  7700  wfrlem4OLD  7701  wfrlem12  7709  oaabs  8008  eceqoveq  8136  php3  8434  pssinf  8458  unbnn2  8505  inf0  8815  inf3lem5  8826  tcel  8918  rankxpsuc  9042  carduni  9140  prdom2  9162  dfac5  9284  cflm  9407  indpi  10064  prlem934  10190  negf1o  10805  xrub  12454  injresinjlem  12907  hashgt12el  13524  hashgt12el2  13525  fi1uzind  13593  swrdwrdsymb  13766  cshwcsh2id  13979  cshwshash  16210  dfgrp2  17834  symgextf1  18224  gsummoncoe1  20070  basis2  21163  fbdmn0  22046  rusgr1vtxlem  26935  clwwlknun  27528  conngrv2edg  27612  frcond1  27688  4cyclusnfrgr  27714  atcv0eq  29824  dfon2lem9  32298  trpredrec  32340  frmin  32345  frrlem4  32386  altopthsn  32671  rankeq1o  32881  bj-currypeirce  33138  bj-cbvalimt  33211  bj-cbveximt  33212  wl-orel12  33903  wl-equsb4  33947  rngoueqz  34357  hbtlem5  38649  ntrk0kbimka  39285  funressnfv  42099  afvco2  42209  ndmaovcl  42236  bgoldbtbndlem4  42713  rngdir  42889  zlmodzxznm  43293