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

Theorem syl5ibcom 153
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 152 . 2 (𝜒 → (𝜑𝜃))
43com12 30 1 (𝜑 → (𝜒𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  biimpcd  157  mob2  2786  rmob  2920  preqr1g  3593  issod  4119  sotritrieq  4125  nsuceq0g  4218  suctr  4221  nordeq  4332  suc11g  4345  iss  4724  poirr2  4788  xp11m  4832  tz6.12c  5291  fnbrfvb  5302  fvelimab  5317  foeqcnvco  5524  f1eqcocnv  5525  acexmidlemcase  5602  nna0r  6187  nnawordex  6233  ectocld  6304  ecoptocl  6325  mapsn  6393  eqeng  6429  fopwdom  6498  ordiso  6666  ltexnqq  6904  nsmallnqq  6908  nqprloc  7041  aptiprleml  7135  0re  7425  lttri3  7502  0cnALT  7609  reapti  7990  recnz  8765  zneo  8773  uzn0  8959  flqidz  9614  ceilqidz  9644  modqid2  9679  modqmuladdnn0  9696  frec2uzrand  9733  frecuzrdgtcl  9740  iseqid  9835  iseqz  9838  facdiv  10035  facwordi  10037  maxleb  10537  fsumf1o  10661  dvdsnegb  10680  odd2np1lem  10739  odd2np1  10740  ltoddhalfle  10760  halfleoddlt  10761  opoe  10762  omoe  10763  opeo  10764  omeo  10765  gcddiv  10875  gcdzeq  10878  dvdssqim  10880  lcmgcdeq  10932  coprmdvds2  10942  rpmul  10947  divgcdcoprmex  10951  cncongr2  10953  dvdsprm  10985  coprm  10990  prmdvdsexp  10994  bj-peano4  11280
  Copyright terms: Public domain W3C validator