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

Theorem syl5ibcom 154
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 153 . 2 (𝜒 → (𝜑𝜃))
43com12 30 1 (𝜑 → (𝜒𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  biimpcd  158  mob2  2835  rmob  2971  preqr1g  3661  issod  4209  sotritrieq  4215  nsuceq0g  4308  suctr  4311  nordeq  4427  suc11g  4440  iss  4833  poirr2  4899  xp11m  4945  tz6.12c  5417  fnbrfvb  5428  fvelimab  5443  foeqcnvco  5657  f1eqcocnv  5658  acexmidlemcase  5735  nna0r  6340  nnawordex  6390  ectocld  6461  ecoptocl  6482  mapsn  6550  eqeng  6626  fopwdom  6696  ordiso  6887  ltexnqq  7180  nsmallnqq  7184  nqprloc  7317  aptiprleml  7411  map2psrprg  7577  0re  7730  lttri3  7808  0cnALT  7916  reapti  8304  recnz  9095  zneo  9103  uzn0  9290  flqidz  9999  ceilqidz  10029  modqid2  10064  modqmuladdnn0  10081  frec2uzrand  10118  frecuzrdgtcl  10125  seq3id  10221  seq3z  10224  facdiv  10424  facwordi  10426  maxleb  10928  fsumf1o  11099  dvdsnegb  11406  odd2np1lem  11465  odd2np1  11466  ltoddhalfle  11486  halfleoddlt  11487  opoe  11488  omoe  11489  opeo  11490  omeo  11491  gcddiv  11603  gcdzeq  11606  dvdssqim  11608  lcmgcdeq  11660  coprmdvds2  11670  rpmul  11675  divgcdcoprmex  11679  cncongr2  11681  dvdsprm  11713  coprm  11718  prmdvdsexp  11722  exmidunben  11834  baspartn  12112  bastop  12139  isopn3  12189  bj-peano4  12964  sbthomlem  13031
  Copyright terms: Public domain W3C validator