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  6506  genpassl  6507  genpassu  6508  ltpopr  6567  ltexprlemm  6572  ltexprlemdisj  6578  ltexprlemloc  6579  letri3  6856  letr  6858  ltneg  7212  leneg  7215  reapltxor  7333  apsym  7350  elnnnn0  7961  zrevaddcl  8031  znnsub  8032  znn0sub  8045  prime  8073  eluz2  8215  eluz2b1  8275  nn01to3  8288  qrevaddcl  8313  xrletri3  8451  xrletr  8454  iccid  8524  elicopnf  8568  fzsplit2  8644  fzsn  8659  fzpr  8669  uzsplit  8684  lt2sqi  8954  le2sqi  8955  bj-sseq  9200
  Copyright terms: Public domain W3C validator