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  3106  2rmorex  3762  ssprsseq  4829  preqsnd  4863  elpr2elpr  4873  disjxiun  5144  oprabidw  7461  oprabid  7462  elovmporab  7678  elovmporab1w  7679  elovmporab1  7680  mpoxopoveqd  8244  wfr3g  8345  oewordri  8628  fsuppunbi  9426  frr3g  9793  r1sdom  9811  updjud  9971  pr2neOLD  10042  kmlem4  10191  kmlem12  10199  domtriomlem  10479  zorn2lem6  10538  axdclem  10556  wunr1om  10756  tskr1om  10804  zindd  12716  hash2pwpr  14511  fi1uzind  14542  swrdnd0  14691  pfxccatin12  14767  repsdf2  14812  2cshwcshw  14860  cshwcshid  14862  fprodmodd  16029  alzdvds  16353  pwp1fsum  16424  lcmfdvds  16675  prm23ge5  16848  cshwshashlem2  17130  0ringnnzr  20541  01eq0ringOLD  20547  ringcbasbas  20689  psgndiflemA  21636  mplcoe5lem  22074  gsummoncoe1  22327  gsummatr01lem3  22678  mp2pm2mplem4  22830  fiinopn  22922  cnmptcom  23701  fgcl  23901  fmfnfmlem1  23977  fmco  23984  flffbas  24018  cnpflf2  24023  metcnp3  24568  tngngp3  24692  clmvscom  25136  cphsscph  25298  aalioulem2  26389  elntg2  29014  ausgrusgrb  29196  usgredg4  29248  nbgr1vtx  29389  uhgr0edg0rgrb  29606  uhgrwkspth  29787  usgr2wlkspth  29791  uspgrn2crct  29837  crctcshwlkn0  29850  wwlksnredwwlkn  29924  wwlksnextsurj  29929  hashecclwwlkn1  30105  umgrhashecclwwlk  30106  frgrnbnb  30321  frgrwopreglem5  30349  frgrwopreglem5ALT  30350  cvati  32394  dmdbr5ati  32450  loop1cycl  35121  sat1el2xp  35363  antnest  35673  dfon2lem3  35766  bj-peircestab  36535  bj-0int  37083  ptrecube  37606  fzmul  37727  zerdivemp1x  37933  psshepw  43777  ndmaovdistr  47156  ssfz12  47263  fzopredsuc  47272  smonoord  47295  elsetpreimafvbi  47315  iccpartltu  47349  iccpartgtl  47350  ichreuopeq  47397  elsprel  47399  lighneallem3  47531  odd2prm2  47642  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  bgoldbnnsum3prm  47728  clnbgrgrimlem  47838  grtrif1o  47846  grtriclwlk3  47849  ringcbasbasALTV  48155  ply1mulgsumlem2  48232  ldepsnlinclem1  48350  ldepsnlinclem2  48351  nnolog2flm1  48439  blengt1fldiv2p1  48442