Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl5ibcom GIF version

Theorem syl5ibcom 148
 Description: A mixed syllogism inference. (Contributed by NM, 19-Jun-2007.)
Hypotheses
Ref Expression
syl5ib.1 (𝜑𝜓)
syl5ib.2 (𝜒 → (𝜓𝜃))
Assertion
Ref Expression
syl5ibcom (𝜑 → (𝜒𝜃))

Proof of Theorem syl5ibcom
StepHypRef Expression
1 syl5ib.1 . . 3 (𝜑𝜓)
2 syl5ib.2 . . 3 (𝜒 → (𝜓𝜃))
31, 2syl5ib 147 . 2 (𝜒 → (𝜑𝜃))
43com12 30 1 (𝜑 → (𝜒𝜃))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 102 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  biimpcd  152  mob2  2744  rmob  2878  preqr1g  3565  issod  4084  sotritrieq  4090  nsuceq0g  4183  suctr  4186  nordeq  4296  suc11g  4309  iss  4682  poirr2  4745  xp11m  4787  tz6.12c  5231  fnbrfvb  5242  fvelimab  5257  foeqcnvco  5458  f1eqcocnv  5459  acexmidlemcase  5535  nna0r  6088  nnawordex  6132  ectocld  6203  ecoptocl  6224  eqeng  6277  fopwdom  6341  ordiso  6416  ltexnqq  6564  nsmallnqq  6568  nqprloc  6701  aptiprleml  6795  0re  7085  lttri3  7157  0cnALT  7264  reapti  7644  recnz  8391  zneo  8398  uzn0  8584  flqidz  9236  ceilqidz  9266  modqid2  9301  modqmuladdnn0  9318  frec2uzrand  9355  frecuzrdgfn  9362  iseqid  9411  iseqz  9413  facdiv  9606  facwordi  9608  dvdsnegb  10125  odd2np1lem  10183  odd2np1  10184  ltoddhalfle  10205  halfleoddlt  10206  opoe  10207  omoe  10208  opeo  10209  omeo  10210  bj-peano4  10467
 Copyright terms: Public domain W3C validator