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  3099  2rmorex  3747  ssprsseq  4824  preqsnd  4857  elpr2elpr  4867  disjxiun  5142  oprabidw  7447  oprabid  7448  elovmporab  7664  elovmporab1w  7665  elovmporab1  7666  mpoxopoveqd  8228  wfr3g  8329  oewordri  8614  fsuppunbi  9425  frr3g  9792  r1sdom  9810  updjud  9970  pr2neOLD  10041  kmlem4  10189  kmlem12  10197  domtriomlem  10476  zorn2lem6  10535  axdclem  10553  wunr1om  10753  tskr1om  10801  zindd  12709  hash2pwpr  14490  fi1uzind  14511  swrdnd0  14660  pfxccatin12  14736  repsdf2  14781  2cshwcshw  14829  cshwcshid  14831  fprodmodd  15994  alzdvds  16317  pwp1fsum  16388  lcmfdvds  16638  prm23ge5  16812  cshwshashlem2  17094  0ringnnzr  20503  01eq0ringOLD  20509  ringcbasbas  20647  psgndiflemA  21593  mplcoe5lem  22042  gsummoncoe1  22296  gsummatr01lem3  22647  mp2pm2mplem4  22799  fiinopn  22891  cnmptcom  23670  fgcl  23870  fmfnfmlem1  23946  fmco  23953  flffbas  23987  cnpflf2  23992  metcnp3  24537  tngngp3  24661  clmvscom  25105  cphsscph  25267  aalioulem2  26358  elntg2  28916  ausgrusgrb  29098  usgredg4  29150  nbgr1vtx  29291  uhgr0edg0rgrb  29508  uhgrwkspth  29689  usgr2wlkspth  29693  uspgrn2crct  29739  crctcshwlkn0  29752  wwlksnredwwlkn  29826  wwlksnextsurj  29831  hashecclwwlkn1  30007  umgrhashecclwwlk  30008  frgrnbnb  30223  frgrwopreglem5  30251  frgrwopreglem5ALT  30252  cvati  32296  dmdbr5ati  32352  loop1cycl  34978  sat1el2xp  35220  dfon2lem3  35622  bj-peircestab  36269  bj-0int  36821  ptrecube  37334  fzmul  37455  zerdivemp1x  37661  psshepw  43492  ndmaovdistr  46856  ssfz12  46963  fzopredsuc  46972  smonoord  46979  elsetpreimafvbi  46999  iccpartltu  47033  iccpartgtl  47034  ichreuopeq  47081  elsprel  47083  lighneallem3  47215  odd2prm2  47326  nnsum4primeseven  47408  nnsum4primesevenALTV  47409  bgoldbnnsum3prm  47412  clnbgrgrimlem  47516  ringcbasbasALTV  47725  ply1mulgsumlem2  47806  ldepsnlinclem1  47924  ldepsnlinclem2  47925  nnolog2flm1  48014  blengt1fldiv2p1  48017