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 ⊢ (𝜓 → (𝜃 → 𝜒))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  imbibi  395  2rmorex  3726  ssprsseq  4792  preqsnd  4825  elpr2elpr  4835  disjxiun  5107  oprabidw  7439  oprabid  7440  elovmporab  7654  elovmporab1w  7655  elovmporab1  7656  mpoxopoveqd  8213  wfr3g  8312  oewordri  8574  fsuppunbi  9345  frr3g  9724  r1sdom  9742  updjud  9916  kmlem4  10133  kmlem12  10141  domtriomlem  10422  zorn2lem6  10481  axdclem  10499  wunr1om  10700  tskr1om  10748  zindd  12693  hash2pwpr  14509  fi1uzind  14540  swrdnd0  14691  pfxccatin12  14766  repsdf2  14811  2cshwcshw  14858  cshwcshid  14860  fprodmodd  16047  alzdvds  16374  pwp1fsum  16445  lcmfdvds  16696  prm23ge5  16871  cshwshashlem2  17152  0ringnnzr  20605  01eq0ringOLD  20611  ringcbasbas  20754  psgndiflemA  21716  mplcoe5lem  22155  gsummoncoe1  22433  gsummatr01lem3  22779  mp2pm2mplem4  22931  fiinopn  23023  cnmptcom  23800  fgcl  24000  fmfnfmlem1  24076  fmco  24083  flffbas  24117  cnpflf2  24122  metcnp3  24662  tngngp3  24778  clmvscom  25214  cphsscph  25375  aalioulem2  26459  elntg2  29272  ausgrusgrb  29452  usgredg4  29504  nbgr1vtx  29645  uhgr0edg0rgrb  29861  uhgrwkspth  30041  usgr2wlkspth  30045  uspgrn2crct  30094  crctcshwlkn0  30107  wwlksnredwwlkn  30181  wwlksnextsurj  30186  hashecclwwlkn1  30365  umgrhashecclwwlk  30366  frgrnbnb  30581  frgrwopreglem5  30609  frgrwopreglem5ALT  30610  cvati  32655  dmdbr5ati  32711  loop1cycl  35524  sat1el2xp  35766  antnest  36076  dfon2lem3  36170  bj-peircestab  37028  bj-0int  37626  ptrecube  38154  fzmul  38275  zerdivemp1x  38481  psshepw  44399  ndmaovdistr  47826  ssfz12  47933  fzopredsuc  47943  smonoord  47996  elsetpreimafvbi  48022  iccpartltu  48056  iccpartgtl  48057  ichreuopeq  48104  elsprel  48106  lighneallem3  48241  odd2prm2  48365  nnsum4primeseven  48447  nnsum4primesevenALTV  48448  bgoldbnnsum3prm  48451  clnbgrgrimlem  48580  grtrif1o  48589  grtriclwlk3  48592  gpgprismgr4cycllem7  48748  pgnbgreunbgr  48772  ringcbasbasALTV  48959  ply1mulgsumlem2  49045  ldepsnlinclem1  49163  ldepsnlinclem2  49164  nnolog2flm1  49248  blengt1fldiv2p1  49251