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

Theorem syl5ibr 154
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 139 . 2 (𝜒 → (𝜃𝜓))
41, 3syl5ib 152 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  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  syl5ibrcom  155  biimprd  156  nbn2  646  limelon  4200  eldifpw  4272  ssonuni  4278  onsucuni2  4353  peano2  4383  limom  4401  elrnmpt1  4654  cnveqb  4852  cnveq0  4853  relcoi1  4928  ndmfvg  5298  ffvresb  5424  caovord3d  5772  poxp  5954  nnm0r  6194  nnacl  6195  nnacom  6199  nnaass  6200  nndi  6201  nnmass  6202  nnmsucr  6203  nnmcom  6204  brecop  6334  ecopovtrn  6341  ecopovtrng  6344  elpm2r  6375  map0g  6397  fundmen  6475  mapxpen  6516  phpm  6533  f1vrnfibi  6604  mulcmpblnq  6871  ordpipqqs  6877  mulcmpblnq0  6947  genpprecll  7017  genppreclu  7018  addcmpblnr  7229  ax1rid  7356  axpre-mulgt0  7366  cnegexlem1  7601  msqge0  8034  mulge0  8037  ltleap  8048  nnmulcl  8378  nnsub  8395  elnn0z  8696  ztri3or0  8725  nneoor  8781  uz11  8973  xltnegi  9229  frec2uzuzd  9737  iseqss  9799  iseqsst  9800  iseqfveq2  9802  iseqshft2  9806  iseqsplit  9812  iseqcaopr3  9814  iseqid2  9843  iseqhomo  9844  m1expcl2  9875  expadd  9895  expmul  9898  faclbnd  10045  hashfzp1  10128  hashfacen  10137  iseqcoll  10143  caucvgrelemcau  10308  recan  10437  rexanre  10548  dvdstr  10708  alzdvds  10730  zob  10766  gcdmultiplez  10885  dvdssq  10895  cncongr2  10961  bj-om  11270  bj-inf2vnlem2  11304  bj-inf2vn  11307  bj-inf2vn2  11308
  Copyright terms: Public domain W3C validator