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

Theorem syl5ibcom 153
Description: A mixed syllogism inference. (Contributed by NM, 19-Jun-2007.)
Hypotheses
Ref Expression
syl5ib.1  |-  ( ph  ->  ps )
syl5ib.2  |-  ( ch 
->  ( ps  <->  th )
)
Assertion
Ref Expression
syl5ibcom  |-  ( ph  ->  ( ch  ->  th )
)

Proof of Theorem syl5ibcom
StepHypRef Expression
1 syl5ib.1 . . 3  |-  ( ph  ->  ps )
2 syl5ib.2 . . 3  |-  ( ch 
->  ( ps  <->  th )
)
31, 2syl5ib 152 . 2  |-  ( ch 
->  ( ph  ->  th )
)
43com12 30 1  |-  ( ph  ->  ( ch  ->  th )
)
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  2793  rmob  2929  preqr1g  3605  issod  4137  sotritrieq  4143  nsuceq0g  4236  suctr  4239  nordeq  4350  suc11g  4363  iss  4745  poirr2  4811  xp11m  4856  tz6.12c  5318  fnbrfvb  5329  fvelimab  5344  foeqcnvco  5551  f1eqcocnv  5552  acexmidlemcase  5629  nna0r  6221  nnawordex  6267  ectocld  6338  ecoptocl  6359  mapsn  6427  eqeng  6463  fopwdom  6532  ordiso  6708  ltexnqq  6946  nsmallnqq  6950  nqprloc  7083  aptiprleml  7177  0re  7467  lttri3  7544  0cnALT  7651  reapti  8032  recnz  8809  zneo  8817  uzn0  9003  flqidz  9658  ceilqidz  9688  modqid2  9723  modqmuladdnn0  9740  frec2uzrand  9777  frecuzrdgtcl  9784  iseqid  9904  iseqz  9908  facdiv  10111  facwordi  10113  maxleb  10614  fsumf1o  10746  dvdsnegb  10906  odd2np1lem  10965  odd2np1  10966  ltoddhalfle  10986  halfleoddlt  10987  opoe  10988  omoe  10989  opeo  10990  omeo  10991  gcddiv  11101  gcdzeq  11104  dvdssqim  11106  lcmgcdeq  11158  coprmdvds2  11168  rpmul  11173  divgcdcoprmex  11177  cncongr2  11179  dvdsprm  11211  coprm  11216  prmdvdsexp  11220  bj-peano4  11507
  Copyright terms: Public domain W3C validator