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

Theorem syl6ibr 161
Description: A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded consequent with a definition. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl6ibr.1 (𝜑 → (𝜓𝜒))
syl6ibr.2 (𝜃𝜒)
Assertion
Ref Expression
syl6ibr (𝜑 → (𝜓𝜃))

Proof of Theorem syl6ibr
StepHypRef Expression
1 syl6ibr.1 . 2 (𝜑 → (𝜓𝜒))
2 syl6ibr.2 . . 3 (𝜃𝜒)
32biimpri 132 . 2 (𝜒𝜃)
41, 3syl6 33 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:  3imtr4g  204  imp4a  346  dcbi  905  oplem1  944  3impexpbicom  1399  hband  1450  hb3and  1451  nfand  1532  nfimd  1549  equsexd  1692  euim  2045  mopick2  2060  2moswapdc  2067  necon3bd  2328  necon3d  2329  necon2ad  2342  necon1abiddc  2347  ralrimd  2487  rspcimedv  2765  2reuswapdc  2861  ra5  2969  difin  3283  r19.2m  3419  r19.2mOLD  3420  tpid3g  3608  sssnm  3651  ssiun  3825  ssiun2  3826  disjnim  3890  exmidsssnc  4096  sotricim  4215  sotritrieq  4217  tron  4274  ordsucss  4390  ordunisuc2r  4400  ordpwsucss  4452  dmcosseq  4780  relssres  4827  trin2  4900  ssrnres  4951  fnun  5199  f1oun  5355  ssimaex  5450  chfnrn  5499  dffo4  5536  dffo5  5537  isoselem  5689  fnoprabg  5840  poxp  6097  issmo2  6154  smores  6157  tfr0dm  6187  tfrlemibxssdm  6192  tfr1onlembxssdm  6208  tfrcllembxssdm  6221  swoer  6425  qsss  6456  findcard  6750  findcard2  6751  findcard2s  6752  supmoti  6848  ctmlemr  6961  ctm  6962  pm54.43  7014  indpi  7118  recexprlemm  7400  recexprlemloc  7407  recexprlem1ssl  7409  recexprlem1ssu  7410  recexprlemss1l  7411  recexprlemss1u  7412  zmulcl  9075  indstr  9356  eluzdc  9372  icoshft  9741  fzouzsplit  9924  hashunlem  10518  modfsummod  11195  dvds2lem  11432  oddnn02np1  11504  dfgcd2  11629  sqrt2irr  11767  ennnfonelemhom  11855  distop  12181  epttop  12186  restdis  12280  cnrest2  12332  cnptopresti  12334  uptx  12370  txcn  12371  decidr  12930  bj-omssind  13060  bj-om  13062  bj-inf2vnlem3  13097  bj-inf2vnlem4  13098
  Copyright terms: Public domain W3C validator