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  3712  ssprsseq  4786  preqsnd  4819  elpr2elpr  4829  disjxiun  5100  oprabidw  7444  oprabid  7445  elovmporab  7660  elovmporab1w  7661  elovmporab1  7662  mpoxopoveqd  8219  wfr3g  8318  oewordri  8580  fsuppunbi  9359  frr3g  9738  r1sdom  9756  updjud  9939  kmlem4  10156  kmlem12  10164  domtriomlem  10444  zorn2lem6  10503  axdclem  10521  wunr1om  10728  tskr1om  10776  zindd  12722  hash2pwpr  14541  fi1uzind  14572  swrdnd0  14727  pfxccatin12  14802  repsdf2  14849  2cshwcshw  14896  cshwcshid  14898  fprodmodd  16084  alzdvds  16410  pwp1fsum  16481  lcmfdvds  16732  prm23ge5  16907  cshwshashlem2  17188  0ringnnzr  20686  01eq0ringOLD  20692  ringcbasbas  20835  isfieldidl  21449  psgndiflemA  21814  mplcoe5lem  22255  gsummoncoe1  22533  gsummatr01lem3  22879  mp2pm2mplem4  23034  fiinopn  23126  cnmptcom  23904  fgcl  24104  fmfnfmlem1  24180  fmco  24187  flffbas  24221  cnpflf2  24226  metcnp3  24766  tngngp3  24882  clmvscom  25318  cphsscph  25479  aalioulem2  26569  elntg2  29442  ausgrusgrb  29625  usgredg4  29677  nbgr1vtx  29818  uhgr0edg0rgrb  30034  uhgrwkspth  30220  usgr2wlkspth  30224  uspgrn2crct  30276  crctcshwlkn0  30289  wwlksnredwwlkn  30363  wwlksnextsurj  30368  hashecclwwlkn1  30547  umgrhashecclwwlk  30548  loop1cycl  30623  frgrnbnb  30773  frgrwopreglem5  30801  frgrwopreglem5ALT  30802  cvati  32847  dmdbr5ati  32903  sat1el2xp  35958  antnest  36268  dfon2lem3  36362  bj-peircestab  37251  bj-0int  37851  ptrecube  38369  fzmul  38491  zerdivemp1x  38697  psshepw  44628  ndmaovdistr  48095  ssfz12  48202  fzopredsuc  48212  smonoord  48265  elsetpreimafvbi  48291  iccpartltu  48325  iccpartgtl  48326  ichreuopeq  48373  elsprel  48375  lighneallem3  48510  odd2prm2  48634  nnsum4primeseven  48716  nnsum4primesevenALTV  48717  bgoldbnnsum3prm  48720  clnbgrgrimlem  48849  grtrif1o  48858  grtriclwlk3  48861  gpgprismgr4cycllem7  49017  pgnbgreunbgr  49041  ringcbasbasALTV  49227  ply1mulgsumlem2  49317  ldepsnlinclem1  49435  ldepsnlinclem2  49436  nnolog2flm1  49520  blengt1fldiv2p1  49523