Theorem syl11 34

Description: A syllogism inference. Commuted form of an instance of syl 18. (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 18	. 2 ⊢ (𝜃 → (𝜓 → 𝜒))
4	3	com12 33	1 ⊢ (𝜓 → (𝜃 → 𝜒))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  imbibi  396  2rmorex  3719  ssprsseq  4793  preqsnd  4826  elpr2elpr  4836  disjxiun  5108  oprabidw  7447  oprabid  7448  elovmporab  7662  elovmporab1w  7663  elovmporab1  7664  mpoxopoveqd  8219  wfr3g  8318  oewordri  8580  fsuppunbi  9352  frr3g  9731  r1sdom  9749  updjud  9932  kmlem4  10149  kmlem12  10157  domtriomlem  10437  zorn2lem6  10496  axdclem  10514  wunr1om  10715  tskr1om  10763  zindd  12708  hash2pwpr  14526  fi1uzind  14557  swrdnd0  14712  pfxccatin12  14787  repsdf2  14834  2cshwcshw  14881  cshwcshid  14883  fprodmodd  16069  alzdvds  16395  pwp1fsum  16466  lcmfdvds  16717  prm23ge5  16892  cshwshashlem2  17173  0ringnnzr  20652  01eq0ringOLD  20658  ringcbasbas  20801  isfieldidl  21415  psgndiflemA  21780  mplcoe5lem  22219  gsummoncoe1  22497  gsummatr01lem3  22843  mp2pm2mplem4  22995  fiinopn  23087  cnmptcom  23864  fgcl  24064  fmfnfmlem1  24140  fmco  24147  flffbas  24181  cnpflf2  24186  metcnp3  24726  tngngp3  24842  clmvscom  25278  cphsscph  25439  aalioulem2  26525  elntg2  29364  ausgrusgrb  29544  usgredg4  29596  nbgr1vtx  29737  uhgr0edg0rgrb  29953  uhgrwkspth  30133  usgr2wlkspth  30137  uspgrn2crct  30186  crctcshwlkn0  30199  wwlksnredwwlkn  30273  wwlksnextsurj  30278  hashecclwwlkn1  30457  umgrhashecclwwlk  30458  frgrnbnb  30673  frgrwopreglem5  30701  frgrwopreglem5ALT  30702  cvati  32747  dmdbr5ati  32803  loop1cycl  35642  sat1el2xp  35884  antnest  36194  dfon2lem3  36288  bj-peircestab  37176  bj-0int  37776  ptrecube  38304  fzmul  38425  zerdivemp1x  38631  psshepw  44547  ndmaovdistr  47977  ssfz12  48084  fzopredsuc  48094  smonoord  48147  elsetpreimafvbi  48173  iccpartltu  48207  iccpartgtl  48208  ichreuopeq  48255  elsprel  48257  lighneallem3  48392  odd2prm2  48516  nnsum4primeseven  48598  nnsum4primesevenALTV  48599  bgoldbnnsum3prm  48602  clnbgrgrimlem  48731  grtrif1o  48740  grtriclwlk3  48743  gpgprismgr4cycllem7  48899  pgnbgreunbgr  48923  ringcbasbasALTV  49110  ply1mulgsumlem2  49200  ldepsnlinclem1  49318  ldepsnlinclem2  49319  nnolog2flm1  49403  blengt1fldiv2p1  49406