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  3115  2rmorex  3776  ssprsseq  4850  preqsnd  4883  elpr2elpr  4893  disjxiun  5163  oprabidw  7479  oprabid  7480  elovmporab  7696  elovmporab1w  7697  elovmporab1  7698  mpoxopoveqd  8262  wfr3g  8363  oewordri  8648  fsuppunbi  9458  frr3g  9825  r1sdom  9843  updjud  10003  pr2neOLD  10074  kmlem4  10223  kmlem12  10231  domtriomlem  10511  zorn2lem6  10570  axdclem  10588  wunr1om  10788  tskr1om  10836  zindd  12744  hash2pwpr  14525  fi1uzind  14556  swrdnd0  14705  pfxccatin12  14781  repsdf2  14826  2cshwcshw  14874  cshwcshid  14876  fprodmodd  16045  alzdvds  16368  pwp1fsum  16439  lcmfdvds  16689  prm23ge5  16862  cshwshashlem2  17144  0ringnnzr  20551  01eq0ringOLD  20557  ringcbasbas  20695  psgndiflemA  21642  mplcoe5lem  22080  gsummoncoe1  22333  gsummatr01lem3  22684  mp2pm2mplem4  22836  fiinopn  22928  cnmptcom  23707  fgcl  23907  fmfnfmlem1  23983  fmco  23990  flffbas  24024  cnpflf2  24029  metcnp3  24574  tngngp3  24698  clmvscom  25142  cphsscph  25304  aalioulem2  26393  elntg2  29018  ausgrusgrb  29200  usgredg4  29252  nbgr1vtx  29393  uhgr0edg0rgrb  29610  uhgrwkspth  29791  usgr2wlkspth  29795  uspgrn2crct  29841  crctcshwlkn0  29854  wwlksnredwwlkn  29928  wwlksnextsurj  29933  hashecclwwlkn1  30109  umgrhashecclwwlk  30110  frgrnbnb  30325  frgrwopreglem5  30353  frgrwopreglem5ALT  30354  cvati  32398  dmdbr5ati  32454  loop1cycl  35105  sat1el2xp  35347  dfon2lem3  35749  bj-peircestab  36519  bj-0int  37067  ptrecube  37580  fzmul  37701  zerdivemp1x  37907  psshepw  43750  ndmaovdistr  47122  ssfz12  47229  fzopredsuc  47238  smonoord  47245  elsetpreimafvbi  47265  iccpartltu  47299  iccpartgtl  47300  ichreuopeq  47347  elsprel  47349  lighneallem3  47481  odd2prm2  47592  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  bgoldbnnsum3prm  47678  clnbgrgrimlem  47785  grtrif1o  47793  grtriclwlk3  47796  ringcbasbasALTV  48035  ply1mulgsumlem2  48116  ldepsnlinclem1  48234  ldepsnlinclem2  48235  nnolog2flm1  48324  blengt1fldiv2p1  48327