Theorem syl6com 36

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 34	. 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  1802  ax6e  2238  axc16i  2310  rgen2a  2960  wefrc  5032  elres  5355  sorpssuni  6844  sorpssint  6845  ordzsl  6937  limuni3  6944  funcnvuni  7012  funrnex  7026  soxp  7177  wfrlem4  7305  wfrlem12  7313  oaabs  7611  eceqoveq  7740  php3  8031  pssinf  8055  unbnn2  8102  inf0  8401  inf3lem5  8412  tcel  8504  rankxpsuc  8628  carduni  8690  prdom2  8712  dfac5  8834  cflm  8955  indpi  9608  prlem934  9734  negf1o  10339  xrub  12014  injresinjlem  12450  hashgt12el  13070  hashgt12el2  13071  fi1uzind  13134  fi1uzindOLD  13140  cshwcsh2id  13425  cshwshash  15649  dfgrp2  17270  symgextf1  17664  gsummoncoe1  19495  basis2  20566  fbdmn0  21448  usgranloopv  25907  nbgranself2  25965  usgrwlknloop  26093  wlkdvspthlem  26137  4cyclusnfrgra  26546  frgrancvvdeqlem7  26563  atcv0eq  28622  dfon2lem9  30940  trpredrec  30982  frmin  30983  frrlem4  31027  frrlem11  31036  altopthsn  31238  rankeq1o  31448  bj-currypeirce  31714  wl-orel12  32473  wl-equsb4  32517  rngoueqz  32909  hbtlem5  36717  ntrk0kbimka  37357  funressnfv  39857  afvco2  39905  ndmaovcl  39932  bgoldbtbndlem4  40224  rusgr1vtxlem  40787  conngrv2edg  41362  frcond1  41438  4cyclusnfrgr  41462  frgrncvvdeqlem7  41475  rngdir  41672  zlmodzxznm  42080