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

Theorem syl5ibr 155
Description: A mixed syllogism inference. (Contributed by NM, 3-Apr-1994.) (Revised by NM, 22-Sep-2013.)
Hypotheses
Ref Expression
syl5ibr.1 (𝜑𝜃)
syl5ibr.2 (𝜒 → (𝜓𝜃))
Assertion
Ref Expression
syl5ibr (𝜒 → (𝜑𝜓))

Proof of Theorem syl5ibr
StepHypRef Expression
1 syl5ibr.1 . 2 (𝜑𝜃)
2 syl5ibr.2 . . 3 (𝜒 → (𝜓𝜃))
32bicomd 140 . 2 (𝜒 → (𝜃𝜓))
41, 3syl5ib 153 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  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  syl5ibrcom  156  biimprd  157  nbn2  686  limelon  4321  eldifpw  4398  ssonuni  4404  onsucuni2  4479  peano2  4509  limom  4527  elrnmpt1  4790  cnveqb  4994  cnveq0  4995  relcoi1  5070  ndmfvg  5452  ffvresb  5583  caovord3d  5941  poxp  6129  nnm0r  6375  nnacl  6376  nnacom  6380  nnaass  6381  nndi  6382  nnmass  6383  nnmsucr  6384  nnmcom  6385  brecop  6519  ecopovtrn  6526  ecopovtrng  6529  elpm2r  6560  map0g  6582  fundmen  6700  mapxpen  6742  phpm  6759  f1vrnfibi  6833  elfir  6861  mulcmpblnq  7188  ordpipqqs  7194  mulcmpblnq0  7264  genpprecll  7334  genppreclu  7335  addcmpblnr  7559  ax1rid  7697  axpre-mulgt0  7707  cnegexlem1  7949  msqge0  8390  mulge0  8393  ltleap  8406  nnmulcl  8753  nnsub  8771  elnn0z  9079  ztri3or0  9108  nneoor  9165  uz11  9360  xltnegi  9630  frec2uzuzd  10187  seq3fveq2  10254  seq3shft2  10258  seq3split  10264  seq3caopr3  10266  seq3id2  10294  seq3homo  10295  m1expcl2  10327  expadd  10347  expmul  10350  faclbnd  10499  hashfzp1  10582  hashfacen  10591  seq3coll  10597  caucvgrelemcau  10764  recan  10893  rexanre  11004  fsumiun  11258  efexp  11400  dvdstr  11541  alzdvds  11563  zob  11599  gcdmultiplez  11720  dvdssq  11730  cncongr2  11796  elrestr  12142  restopn2  12366  txcn  12458  txlm  12462  isxms2  12635  bj-om  13240  bj-inf2vnlem2  13274  bj-inf2vn  13277  bj-inf2vn2  13278
  Copyright terms: Public domain W3C validator