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

Theorem syl5ibrcom 146
 Description: A mixed syllogism inference. (Contributed by NM, 20-Jun-2007.)
Hypotheses
Ref Expression
syl5ibr.1 (𝜑𝜃)
syl5ibr.2 (𝜒 → (𝜓𝜃))
Assertion
Ref Expression
syl5ibrcom (𝜑 → (𝜒𝜓))

Proof of Theorem syl5ibrcom
StepHypRef Expression
1 syl5ibr.1 . . 3 (𝜑𝜃)
2 syl5ibr.2 . . 3 (𝜒 → (𝜓𝜃))
31, 2syl5ibr 145 . 2 (𝜒 → (𝜑𝜓))
43com12 27 1 (𝜑 → (𝜒𝜓))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 98 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  biimprcd  149  elsn2g  3404  preqr1g  3537  opth1  3973  euotd  3991  tz7.2  4091  reusv3  4192  alxfr  4193  reuhypd  4203  ordsucim  4226  suc11g  4281  nlimsucg  4290  onpsssuc  4295  xpsspw  4450  funcnvuni  4968  fvmptdv2  5260  foco2  5318  fsn  5335  fconst2g  5376  funfvima  5390  isores3  5455  eusvobj2  5498  ovmpt2dv2  5634  ovelrn  5649  f1opw2  5706  suppssfv  5708  suppssov1  5709  nnmordi  6089  nnmord  6090  qsss  6165  eroveu  6197  th3qlem1  6208  en1bg  6280  addnidpig  6434  enq0tr  6532  prcdnql  6582  prcunqu  6583  genipv  6607  genpelvl  6610  genpelvu  6611  distrlem5prl  6684  distrlem5pru  6685  aptiprlemu  6738  mulid1  7024  ltne  7103  cnegex  7189  creur  7911  creui  7912  cju  7913  nnsub  7952  un0addcl  8215  un0mulcl  8216  zaddcl  8285  elz2  8312  qmulz  8558  qre  8560  qnegcl  8571  xrltne  8729  iccid  8794  fzsn  8929  fzsuc2  8941  fz1sbc  8958  elfzp12  8961  iseqid3  9245  shftlem  9417  replim  9459  sqrtsq  9642  absle  9685  bj-peano4  10080
 Copyright terms: Public domain W3C validator