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

Theorem syl6ibr 151
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 124 . 2 (χθ)
41, 3syl6 29 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:  3imtr4g  194  imp4a  331  dcbi  843  oplem1  881  3impexpbicom  1324  hband  1375  hb3and  1376  nfand  1457  nfimd  1474  equsexd  1614  euim  1965  mopick2  1980  2moswapdc  1987  necon3bd  2242  necon3d  2243  necon2ad  2256  necon1abiddc  2261  ralrimd  2391  rspcimedv  2652  2reuswapdc  2737  eqsbc3r  2813  ra5  2840  difin  3168  r19.2m  3303  tpid3g  3474  sssnm  3516  ssiun  3690  ssiun2  3691  sotricim  4051  sotritrieq  4053  tron  4085  ordsucss  4196  ordunisuc2r  4205  ordpwsucss  4243  dmcosseq  4546  relssres  4591  trin2  4659  ssrnres  4706  fnun  4948  f1oun  5089  ssimaex  5177  chfnrn  5221  dffo4  5258  dffo5  5259  isoselem  5402  fnoprabg  5544  poxp  5794  issmo2  5845  smores  5848  tfr0  5878  tfrlemibxssdm  5882  swoer  6070  qsss  6101  indpi  6326  recexprlemm  6594  recexprlemloc  6601  recexprlem1ssl  6603  recexprlem1ssu  6604  recexprlemss1l  6605  recexprlemss1u  6606  zmulcl  8033  indstr  8272  eluzdc  8283  icoshft  8588  fzouzsplit  8765  bj-omssind  9323  bj-om  9325  bj-inf2vnlem3  9356  bj-inf2vnlem4  9357
  Copyright terms: Public domain W3C validator