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  1889  19.36imv  1949  sbequ2  2244  nfeqf2  2377  ax6e  2383  axc16i  2436  mo4  2566  rgen2a  3155  rspn0  4283  wefrc  5574  elinxp  5918  sorpssuni  7563  sorpssint  7564  ordzsl  7667  limuni3  7674  funcnvuni  7752  funrnex  7770  soxp  7941  frrlem4  8076  wfrlem4OLD  8114  wfrlem12OLD  8122  oaabs  8438  eceqoveq  8569  php3  8899  pssinf  8962  unbnn2  9001  inf0  9309  inf3lem5  9320  trpredrec  9415  tcel  9434  frmin  9438  rankxpsuc  9571  carduni  9670  prdom2  9693  dfac5  9815  cflm  9937  indpi  10594  prlem934  10720  negf1o  11335  xrub  12975  injresinjlem  13435  hashgt12el  14065  hashgt12el2  14066  fi1uzind  14139  swrdwrdsymb  14303  cshwcsh2id  14469  cshwshash  16734  lidrididd  18269  dfgrp2  18519  symgextf1  18944  gsummoncoe1  21385  basis2  22009  fbdmn0  22893  rusgr1vtxlem  27857  upgrewlkle2  27876  clwwlknun  28377  conngrv2edg  28460  frcond1  28531  4cyclusnfrgr  28557  atcv0eq  30642  dfon2lem9  33673  altopthsn  34190  rankeq1o  34400  bj-cbvalimt  34747  bj-cbveximt  34748  wl-orel12  35597  wl-equsb4  35639  rngoueqz  36025  hbtlem5  40869  ntrk0kbimka  41538  funressnfv  44424  afvco2  44555  ndmaovcl  44582  bgoldbtbndlem4  45148  rngdir  45328  zlmodzxznm  45726