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

Theorem syl5ibr 149
 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 133 . 2 (𝜒 → (𝜃𝜓))
41, 3syl5ib 147 1 (𝜒 → (𝜑𝜓))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 102 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  syl5ibrcom  150  biimprd  151  nbn2  623  limelon  4164  eldifpw  4236  ssonuni  4242  onsucuni2  4316  peano2  4346  limom  4364  elrnmpt1  4613  cnveqb  4804  cnveq0  4805  relcoi1  4877  ndmfvg  5232  ffvresb  5356  caovord3d  5699  poxp  5881  nnm0r  6089  nnacl  6090  nnacom  6094  nnaass  6095  nndi  6096  nnmass  6097  nnmsucr  6098  nnmcom  6099  brecop  6227  ecopovtrn  6234  ecopovtrng  6237  fundmen  6317  phpm  6358  mulcmpblnq  6524  ordpipqqs  6530  mulcmpblnq0  6600  genpprecll  6670  genppreclu  6671  addcmpblnr  6882  ax1rid  7009  axpre-mulgt0  7019  cnegexlem1  7249  msqge0  7681  mulge0  7684  ltleap  7695  nnmulcl  8011  nnsub  8028  elnn0z  8315  ztri3or0  8344  nneoor  8399  uz11  8591  xltnegi  8849  frec2uzuzd  9352  iseqss  9390  iseqfveq2  9392  iseqshft2  9396  iseqsplit  9402  iseqcaopr3  9404  iseqhomo  9412  m1expcl2  9442  expadd  9462  expmul  9465  faclbnd  9609  caucvgrelemcau  9807  recan  9936  dvdstr  10144  alzdvds  10166  zob  10203  bj-om  10448  peano5setOLD  10452  bj-inf2vnlem2  10483  bj-inf2vn  10486  bj-inf2vn2  10487
 Copyright terms: Public domain W3C validator