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  920  oplem1  959  3impexpbicom  1414  hband  1465  hb3and  1466  nfand  1547  nfimd  1564  equsexd  1707  euim  2067  mopick2  2082  2moswapdc  2089  necon3bd  2351  necon3d  2352  necon2ad  2365  necon1abiddc  2370  ralrimd  2510  rspcimedv  2791  2reuswapdc  2888  ra5  2997  difin  3313  r19.2m  3449  r19.2mOLD  3450  tpid3g  3638  sssnm  3681  ssiun  3855  ssiun2  3856  disjnim  3920  exmidsssnc  4126  sotricim  4245  sotritrieq  4247  tron  4304  ordsucss  4420  ordunisuc2r  4430  ordpwsucss  4482  dmcosseq  4810  relssres  4857  trin2  4930  ssrnres  4981  fnun  5229  f1oun  5387  ssimaex  5482  chfnrn  5531  dffo4  5568  dffo5  5569  isoselem  5721  fnoprabg  5872  poxp  6129  issmo2  6186  smores  6189  tfr0dm  6219  tfrlemibxssdm  6224  tfr1onlembxssdm  6240  tfrcllembxssdm  6253  swoer  6457  qsss  6488  findcard  6782  findcard2  6783  findcard2s  6784  supmoti  6880  ctmlemr  6993  ctm  6994  pm54.43  7046  indpi  7157  recexprlemm  7439  recexprlemloc  7446  recexprlem1ssl  7448  recexprlem1ssu  7449  recexprlemss1l  7450  recexprlemss1u  7451  zmulcl  9114  indstr  9395  eluzdc  9411  icoshft  9780  fzouzsplit  9963  hashunlem  10557  modfsummod  11234  dvds2lem  11511  oddnn02np1  11583  dfgcd2  11708  sqrt2irr  11846  ennnfonelemhom  11934  omctfn  11962  distop  12263  epttop  12268  restdis  12362  cnrest2  12414  cnptopresti  12416  uptx  12452  txcn  12453  decidr  13056  bj-omssind  13186  bj-om  13188  bj-inf2vnlem3  13223  bj-inf2vnlem4  13224
 Copyright terms: Public domain W3C validator