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  3109  2rmorex  3760  ssprsseq  4825  preqsnd  4859  elpr2elpr  4869  disjxiun  5140  oprabidw  7462  oprabid  7463  elovmporab  7679  elovmporab1w  7680  elovmporab1  7681  mpoxopoveqd  8246  wfr3g  8347  oewordri  8630  fsuppunbi  9429  frr3g  9796  r1sdom  9814  updjud  9974  pr2neOLD  10045  kmlem4  10194  kmlem12  10202  domtriomlem  10482  zorn2lem6  10541  axdclem  10559  wunr1om  10759  tskr1om  10807  zindd  12719  hash2pwpr  14515  fi1uzind  14546  swrdnd0  14695  pfxccatin12  14771  repsdf2  14816  2cshwcshw  14864  cshwcshid  14866  fprodmodd  16033  alzdvds  16357  pwp1fsum  16428  lcmfdvds  16679  prm23ge5  16853  cshwshashlem2  17134  0ringnnzr  20525  01eq0ringOLD  20531  ringcbasbas  20673  psgndiflemA  21619  mplcoe5lem  22057  gsummoncoe1  22312  gsummatr01lem3  22663  mp2pm2mplem4  22815  fiinopn  22907  cnmptcom  23686  fgcl  23886  fmfnfmlem1  23962  fmco  23969  flffbas  24003  cnpflf2  24008  metcnp3  24553  tngngp3  24677  clmvscom  25123  cphsscph  25285  aalioulem2  26375  elntg2  29000  ausgrusgrb  29182  usgredg4  29234  nbgr1vtx  29375  uhgr0edg0rgrb  29592  uhgrwkspth  29775  usgr2wlkspth  29779  uspgrn2crct  29828  crctcshwlkn0  29841  wwlksnredwwlkn  29915  wwlksnextsurj  29920  hashecclwwlkn1  30096  umgrhashecclwwlk  30097  frgrnbnb  30312  frgrwopreglem5  30340  frgrwopreglem5ALT  30341  cvati  32385  dmdbr5ati  32441  loop1cycl  35142  sat1el2xp  35384  antnest  35694  dfon2lem3  35786  bj-peircestab  36554  bj-0int  37102  ptrecube  37627  fzmul  37748  zerdivemp1x  37954  psshepw  43801  ndmaovdistr  47219  ssfz12  47326  fzopredsuc  47335  smonoord  47358  elsetpreimafvbi  47378  iccpartltu  47412  iccpartgtl  47413  ichreuopeq  47460  elsprel  47462  lighneallem3  47594  odd2prm2  47705  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  bgoldbnnsum3prm  47791  clnbgrgrimlem  47901  grtrif1o  47909  grtriclwlk3  47912  ringcbasbasALTV  48228  ply1mulgsumlem2  48304  ldepsnlinclem1  48422  ldepsnlinclem2  48423  nnolog2flm1  48511  blengt1fldiv2p1  48514