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

Theorem syl6bbr 187
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl6bbr.1 (φ → (ψχ))
syl6bbr.2 (θχ)
Assertion
Ref Expression
syl6bbr (φ → (ψθ))

Proof of Theorem syl6bbr
StepHypRef Expression
1 syl6bbr.1 . 2 (φ → (ψχ))
2 syl6bbr.2 . . 3 (θχ)
32bicomi 123 . 2 (χθ)
41, 3syl6bb 185 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:  3bitr4g  212  bibi2i  216  equsalh  1611  eueq3dc  2709  sbcel12g  2859  sbceqg  2860  sbcnel12g  2861  reldisj  3265  r19.3rm  3304  rabxp  4323  elrng  4469  iss  4597  eliniseg  4638  fcnvres  5016  dffv3g  5117  funimass4  5167  fndmdif  5215  fneqeql  5218  funimass3  5226  elrnrexdmb  5250  dff4im  5256  fconst4m  5324  elunirn  5348  riota1  5429  riota2df  5431  f1ocnvfv3  5444  eqfnov  5549  caoftrn  5678  mpt2xopovel  5797  rntpos  5813  ordgt0ge1  5957  iinerm  6114  erinxp  6116  qliftfun  6124  indpi  6326  genpdflem  6489  genpdisj  6505  genpassl  6506  genpassu  6507  ltpopr  6568  ltexprlemm  6573  ltexprlemdisj  6579  ltexprlemloc  6580  letri3  6876  letr  6878  ltneg  7232  leneg  7235  reapltxor  7353  apsym  7370  elnnnn0  7981  zrevaddcl  8051  znnsub  8052  znn0sub  8065  prime  8093  eluz2  8235  eluz2b1  8295  nn01to3  8308  qrevaddcl  8333  xrletri3  8471  xrletr  8474  iccid  8544  elicopnf  8588  fzsplit2  8664  fzsn  8679  fzpr  8689  uzsplit  8704  lt2sqi  8974  le2sqi  8975  bj-sseq  9246
  Copyright terms: Public domain W3C validator