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.35  3270  2rmorex  3692  ssprsseq  4763  preqsnd  4794  elpr2elpr  4804  disjxiun  5075  oprabidw  7299  oprabid  7300  elovmporab  7506  elovmporab1w  7507  elovmporab1  7508  mpoxopoveqd  8021  wfr3g  8122  oewordri  8399  fsuppunbi  9110  frr3g  9498  r1sdom  9516  updjud  9676  pr2ne  9745  kmlem4  9893  kmlem12  9901  domtriomlem  10182  zorn2lem6  10241  axdclem  10259  wunr1om  10459  tskr1om  10507  zindd  12404  hash2pwpr  14171  fi1uzind  14192  swrdnd0  14351  pfxccatin12  14427  repsdf2  14472  2cshwcshw  14519  cshwcshid  14521  fprodmodd  15688  alzdvds  16010  pwp1fsum  16081  lcmfdvds  16328  prm23ge5  16497  cshwshashlem2  16779  0ringnnzr  20521  01eq0ring  20524  psgndiflemA  20787  mplcoe5lem  21221  gsummoncoe1  21456  gsummatr01lem3  21787  mp2pm2mplem4  21939  fiinopn  22031  cnmptcom  22810  fgcl  23010  fmfnfmlem1  23086  fmco  23093  flffbas  23127  cnpflf2  23132  metcnp3  23677  tngngp3  23801  clmvscom  24234  cphsscph  24396  aalioulem2  25474  elntg2  27334  ausgrusgrb  27516  usgredg4  27565  nbgr1vtx  27706  uhgr0edg0rgrb  27922  uhgrwkspth  28102  usgr2wlkspth  28106  uspgrn2crct  28152  crctcshwlkn0  28165  wwlksnredwwlkn  28239  wwlksnextsurj  28244  hashecclwwlkn1  28420  umgrhashecclwwlk  28421  frgrnbnb  28636  frgrwopreglem5  28664  frgrwopreglem5ALT  28665  cvati  30707  dmdbr5ati  30763  loop1cycl  33078  sat1el2xp  33320  dfon2lem3  33740  bj-peircestab  34712  bj-0int  35251  ptrecube  35756  fzmul  35878  zerdivemp1x  36084  psshepw  41349  ndmaovdistr  44650  ssfz12  44758  fzopredsuc  44767  smonoord  44775  elsetpreimafvbi  44795  iccpartltu  44829  iccpartgtl  44830  ichreuopeq  44877  elsprel  44879  lighneallem3  45011  odd2prm2  45122  nnsum4primeseven  45204  nnsum4primesevenALTV  45205  bgoldbnnsum3prm  45208  ringcbasbas  45544  ringcbasbasALTV  45568  ply1mulgsumlem2  45680  ldepsnlinclem1  45798  ldepsnlinclem2  45799  nnolog2flm1  45888  blengt1fldiv2p1  45891