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:  r19.35OLD  3096  2rmorex  3737  ssprsseq  4801  preqsnd  4835  elpr2elpr  4845  disjxiun  5116  oprabidw  7436  oprabid  7437  elovmporab  7653  elovmporab1w  7654  elovmporab1  7655  mpoxopoveqd  8220  wfr3g  8321  oewordri  8604  fsuppunbi  9401  frr3g  9770  r1sdom  9788  updjud  9948  pr2neOLD  10019  kmlem4  10168  kmlem12  10176  domtriomlem  10456  zorn2lem6  10515  axdclem  10533  wunr1om  10733  tskr1om  10781  zindd  12694  hash2pwpr  14494  fi1uzind  14525  swrdnd0  14675  pfxccatin12  14751  repsdf2  14796  2cshwcshw  14844  cshwcshid  14846  fprodmodd  16013  alzdvds  16339  pwp1fsum  16410  lcmfdvds  16661  prm23ge5  16835  cshwshashlem2  17116  0ringnnzr  20485  01eq0ringOLD  20491  ringcbasbas  20633  psgndiflemA  21561  mplcoe5lem  21997  gsummoncoe1  22246  gsummatr01lem3  22595  mp2pm2mplem4  22747  fiinopn  22839  cnmptcom  23616  fgcl  23816  fmfnfmlem1  23892  fmco  23899  flffbas  23933  cnpflf2  23938  metcnp3  24479  tngngp3  24595  clmvscom  25041  cphsscph  25203  aalioulem2  26293  elntg2  28964  ausgrusgrb  29144  usgredg4  29196  nbgr1vtx  29337  uhgr0edg0rgrb  29554  uhgrwkspth  29737  usgr2wlkspth  29741  uspgrn2crct  29790  crctcshwlkn0  29803  wwlksnredwwlkn  29877  wwlksnextsurj  29882  hashecclwwlkn1  30058  umgrhashecclwwlk  30059  frgrnbnb  30274  frgrwopreglem5  30302  frgrwopreglem5ALT  30303  cvati  32347  dmdbr5ati  32403  loop1cycl  35159  sat1el2xp  35401  antnest  35711  dfon2lem3  35803  bj-peircestab  36571  bj-0int  37119  ptrecube  37644  fzmul  37765  zerdivemp1x  37971  psshepw  43812  ndmaovdistr  47236  ssfz12  47343  fzopredsuc  47352  smonoord  47385  elsetpreimafvbi  47405  iccpartltu  47439  iccpartgtl  47440  ichreuopeq  47487  elsprel  47489  lighneallem3  47621  odd2prm2  47732  nnsum4primeseven  47814  nnsum4primesevenALTV  47815  bgoldbnnsum3prm  47818  clnbgrgrimlem  47946  grtrif1o  47954  grtriclwlk3  47957  gpgprismgr4cycllem7  48100  ringcbasbasALTV  48287  ply1mulgsumlem2  48363  ldepsnlinclem1  48481  ldepsnlinclem2  48482  nnolog2flm1  48570  blengt1fldiv2p1  48573