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

Theorem syl6ibr 155
 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 128 . 2 (𝜒𝜃)
41, 3syl6 33 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:  3imtr4g  198  imp4a  335  dcbi  855  oplem1  893  3impexpbicom  1343  hband  1394  hb3and  1395  nfand  1476  nfimd  1493  equsexd  1633  euim  1984  mopick2  1999  2moswapdc  2006  necon3bd  2263  necon3d  2264  necon2ad  2277  necon1abiddc  2282  ralrimd  2414  rspcimedv  2675  2reuswapdc  2766  ra5  2874  difin  3202  r19.2m  3337  tpid3g  3511  sssnm  3553  ssiun  3727  ssiun2  3728  sotricim  4088  sotritrieq  4090  tron  4147  ordsucss  4258  ordunisuc2r  4268  ordpwsucss  4319  dmcosseq  4631  relssres  4676  trin2  4744  ssrnres  4791  fnun  5033  f1oun  5174  ssimaex  5262  chfnrn  5306  dffo4  5343  dffo5  5344  isoselem  5487  fnoprabg  5630  poxp  5881  issmo2  5935  smores  5938  tfr0  5968  tfrlemibxssdm  5972  swoer  6165  qsss  6196  findcard  6376  findcard2  6377  findcard2s  6378  supmoti  6399  indpi  6498  recexprlemm  6780  recexprlemloc  6787  recexprlem1ssl  6789  recexprlem1ssu  6790  recexprlemss1l  6791  recexprlemss1u  6792  zmulcl  8355  indstr  8632  eluzdc  8644  icoshft  8959  fzouzsplit  9137  dvds2lem  10120  oddnn02np1  10192  sqrt2irr  10251  bj-omssind  10446  bj-om  10448  bj-inf2vnlem3  10484  bj-inf2vnlem4  10485
 Copyright terms: Public domain W3C validator