Theorem syl11 33

Description: A syllogism inference. Commuted form of an instance of syl 17. (Contributed by BJ, 25-Oct-2021.)

Hypotheses

Ref	Expression
syl11.1	⊢ (𝜑 → (𝜓 → 𝜒))
syl11.2	⊢ (𝜃 → 𝜑)

Assertion

Ref	Expression
syl11	⊢ (𝜓 → (𝜃 → 𝜒))

Proof of Theorem syl11

Step	Hyp	Ref	Expression
1		syl11.2	. . 3 ⊢ (𝜃 → 𝜑)
2		syl11.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl 17	. 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:  2rmorex  3713  ssprsseq  4777  preqsnd  4811  elpr2elpr  4821  disjxiun  5088  oprabidw  7377  oprabid  7378  elovmporab  7592  elovmporab1w  7593  elovmporab1  7594  mpoxopoveqd  8151  wfr3g  8249  oewordri  8507  fsuppunbi  9273  frr3g  9649  r1sdom  9667  updjud  9827  kmlem4  10045  kmlem12  10053  domtriomlem  10333  zorn2lem6  10392  axdclem  10410  wunr1om  10610  tskr1om  10658  zindd  12574  hash2pwpr  14383  fi1uzind  14414  swrdnd0  14565  pfxccatin12  14640  repsdf2  14685  2cshwcshw  14732  cshwcshid  14734  fprodmodd  15904  alzdvds  16231  pwp1fsum  16302  lcmfdvds  16553  prm23ge5  16727  cshwshashlem2  17008  0ringnnzr  20441  01eq0ringOLD  20447  ringcbasbas  20589  psgndiflemA  21539  mplcoe5lem  21975  gsummoncoe1  22224  gsummatr01lem3  22573  mp2pm2mplem4  22725  fiinopn  22817  cnmptcom  23594  fgcl  23794  fmfnfmlem1  23870  fmco  23877  flffbas  23911  cnpflf2  23916  metcnp3  24456  tngngp3  24572  clmvscom  25018  cphsscph  25179  aalioulem2  26269  elntg2  28964  ausgrusgrb  29144  usgredg4  29196  nbgr1vtx  29337  uhgr0edg0rgrb  29554  uhgrwkspth  29734  usgr2wlkspth  29738  uspgrn2crct  29787  crctcshwlkn0  29800  wwlksnredwwlkn  29874  wwlksnextsurj  29879  hashecclwwlkn1  30055  umgrhashecclwwlk  30056  frgrnbnb  30271  frgrwopreglem5  30299  frgrwopreglem5ALT  30300  cvati  32344  dmdbr5ati  32400  loop1cycl  35179  sat1el2xp  35421  antnest  35731  dfon2lem3  35825  bj-peircestab  36593  bj-0int  37141  ptrecube  37666  fzmul  37787  zerdivemp1x  37993  psshepw  43827  ndmaovdistr  47244  ssfz12  47351  fzopredsuc  47360  smonoord  47408  elsetpreimafvbi  47428  iccpartltu  47462  iccpartgtl  47463  ichreuopeq  47510  elsprel  47512  lighneallem3  47644  odd2prm2  47755  nnsum4primeseven  47837  nnsum4primesevenALTV  47838  bgoldbnnsum3prm  47841  clnbgrgrimlem  47970  grtrif1o  47979  grtriclwlk3  47982  gpgprismgr4cycllem7  48138  pgnbgreunbgr  48162  ringcbasbasALTV  48349  ply1mulgsumlem2  48425  ldepsnlinclem1  48543  ldepsnlinclem2  48544  nnolog2flm1  48628  blengt1fldiv2p1  48631