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  3110  2rmorex  3750  ssprsseq  4828  preqsnd  4859  elpr2elpr  4869  disjxiun  5145  oprabidw  7437  oprabid  7438  elovmporab  7649  elovmporab1w  7650  elovmporab1  7651  mpoxopoveqd  8203  wfr3g  8304  oewordri  8589  fsuppunbi  9381  frr3g  9748  r1sdom  9766  updjud  9926  pr2neOLD  9997  kmlem4  10145  kmlem12  10153  domtriomlem  10434  zorn2lem6  10493  axdclem  10511  wunr1om  10711  tskr1om  10759  zindd  12660  hash2pwpr  14434  fi1uzind  14455  swrdnd0  14604  pfxccatin12  14680  repsdf2  14725  2cshwcshw  14773  cshwcshid  14775  fprodmodd  15938  alzdvds  16260  pwp1fsum  16331  lcmfdvds  16576  prm23ge5  16745  cshwshashlem2  17027  0ringnnzr  20295  01eq0ringOLD  20299  psgndiflemA  21146  mplcoe5lem  21586  gsummoncoe1  21820  gsummatr01lem3  22151  mp2pm2mplem4  22303  fiinopn  22395  cnmptcom  23174  fgcl  23374  fmfnfmlem1  23450  fmco  23457  flffbas  23491  cnpflf2  23496  metcnp3  24041  tngngp3  24165  clmvscom  24598  cphsscph  24760  aalioulem2  25838  elntg2  28233  ausgrusgrb  28415  usgredg4  28464  nbgr1vtx  28605  uhgr0edg0rgrb  28821  uhgrwkspth  29002  usgr2wlkspth  29006  uspgrn2crct  29052  crctcshwlkn0  29065  wwlksnredwwlkn  29139  wwlksnextsurj  29144  hashecclwwlkn1  29320  umgrhashecclwwlk  29321  frgrnbnb  29536  frgrwopreglem5  29564  frgrwopreglem5ALT  29565  cvati  31607  dmdbr5ati  31663  loop1cycl  34117  sat1el2xp  34359  dfon2lem3  34746  bj-peircestab  35418  bj-0int  35971  ptrecube  36477  fzmul  36598  zerdivemp1x  36804  psshepw  42525  ndmaovdistr  45902  ssfz12  46009  fzopredsuc  46018  smonoord  46026  elsetpreimafvbi  46046  iccpartltu  46080  iccpartgtl  46081  ichreuopeq  46128  elsprel  46130  lighneallem3  46262  odd2prm2  46373  nnsum4primeseven  46455  nnsum4primesevenALTV  46456  bgoldbnnsum3prm  46459  ringcbasbas  46886  ringcbasbasALTV  46910  ply1mulgsumlem2  47022  ldepsnlinclem1  47140  ldepsnlinclem2  47141  nnolog2flm1  47230  blengt1fldiv2p1  47233