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  1899  19.36imv  1959  sbequ2  2278  nfeqf2  2402  ax6e  2408  axc16i  2461  mo4  2587  rgen2a  3352  sbccomlem  3817  rspn0  4303  wefrc  5634  elinxp  5998  sorpssuni  7704  sorpssint  7705  ordzsl  7814  limuni3  7821  funcnvuni  7902  funrnex  7924  soxp  8097  frrlem4  8258  oaabs  8606  eceqoveq  8792  pssinf  9195  unbnn2  9230  inf0  9566  inf3lem5  9577  tcel  9688  frmin  9697  rankxpsuc  9830  carduni  9929  prdom2  9952  dfac5  10075  cflm  10196  indpi  10855  prlem934  10981  negf1o  11607  xrub  13305  injresinjlem  13786  hashgt12el  14425  hashgt12el2  14426  fi1uzind  14510  swrdwrdsymb  14666  cshwcsh2id  14831  cshwshash  17116  lidrididd  18680  dfgrp2  18980  symgextf1  19437  rngdi  20182  rngdir  20183  gsummoncoe1  22344  basis2  22984  fbdmn0  23867  rusgr1vtxlem  29727  upgrewlkle2  29746  clwwlknun  30253  conngrv2edg  30336  frcond1  30407  4cyclusnfrgr  30433  atcv0eq  32521  dfon2lem9  36087  altopthsn  36259  rankeq1o  36469  wl-orel12  37962  wl-equsb4  38008  rngoueqz  38387  hbtlem5  43653  ntrk0kbimka  44563  funressnfv  47585  afvco2  47718  ndmaovcl  47745  bgoldbtbndlem4  48378  isubgr3stgrlem4  48539  zlmodzxznm  49067