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

Theorem syl6bbr 191
 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 127 . 2 (𝜒𝜃)
41, 3syl6bb 189 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:  3bitr4g  216  bibi2i  220  equsalh  1630  eueq3dc  2737  sbcel12g  2892  sbceqg  2893  sbcnel12g  2894  reldisj  3298  r19.3rm  3337  rabxp  4407  elrng  4553  iss  4681  eliniseg  4722  fcnvres  5100  dffv3g  5201  funimass4  5251  fndmdif  5299  fneqeql  5302  funimass3  5310  elrnrexdmb  5334  dff4im  5340  fconst4m  5408  elunirn  5432  riota1  5513  riota2df  5515  f1ocnvfv3  5528  eqfnov  5634  caoftrn  5763  mpt2xopovel  5886  rntpos  5902  ordgt0ge1  6048  iinerm  6208  erinxp  6210  qliftfun  6218  indpi  6497  genpdflem  6662  genpdisj  6678  genpassl  6679  genpassu  6680  ltnqpri  6749  ltpopr  6750  ltexprlemm  6755  ltexprlemdisj  6761  ltexprlemloc  6762  ltrennb  6987  letri3  7157  letr  7159  ltneg  7530  leneg  7533  reapltxor  7653  apsym  7670  elnnnn0  8281  zrevaddcl  8351  znnsub  8352  znn0sub  8366  prime  8395  eluz2  8574  eluz2b1  8634  nn01to3  8648  qrevaddcl  8675  xrletri3  8821  xrletr  8824  iccid  8894  elicopnf  8938  fzsplit2  9015  fzsn  9030  fzpr  9040  uzsplit  9055  fvinim0ffz  9197  lt2sqi  9506  le2sqi  9507  abs00ap  9888  algcvgblem  10250  bj-sseq  10297
 Copyright terms: Public domain W3C validator