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  1813  ax6e  2250  axc16i  2322  rgen2a  2977  wefrc  5108  elres  5435  sorpssuni  6946  sorpssint  6947  ordzsl  7045  limuni3  7052  funcnvuni  7119  funrnex  7133  soxp  7290  wfrlem4  7418  wfrlem12  7426  oaabs  7724  eceqoveq  7853  php3  8146  pssinf  8170  unbnn2  8217  inf0  8518  inf3lem5  8529  tcel  8621  rankxpsuc  8745  carduni  8807  prdom2  8829  dfac5  8951  cflm  9072  indpi  9729  prlem934  9855  negf1o  10460  xrub  12142  injresinjlem  12588  hashgt12el  13210  hashgt12el2  13211  fi1uzind  13279  fi1uzindOLD  13285  cshwcsh2id  13574  cshwshash  15811  dfgrp2  17447  symgextf1  17841  gsummoncoe1  19674  basis2  20755  fbdmn0  21638  rusgr1vtxlem  26483  conngrv2edg  27055  frcond1  27130  4cyclusnfrgr  27156  atcv0eq  29238  dfon2lem9  31696  trpredrec  31738  frmin  31739  frrlem4  31783  frrlem11  31792  altopthsn  32068  rankeq1o  32278  bj-currypeirce  32544  wl-orel12  33294  wl-equsb4  33338  rngoueqz  33739  hbtlem5  37698  ntrk0kbimka  38337  funressnfv  41208  afvco2  41256  ndmaovcl  41283  bgoldbtbndlem4  41696  rngdir  41882  zlmodzxznm  42286