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

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

Proof of Theorem syl5bb
StepHypRef Expression
1 syl5bb.1 . . 3 (φψ)
21a1i 9 . 2 (χ → (φψ))
3 syl5bb.2 . 2 (χ → (ψθ))
42, 3bitrd 177 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:  syl5rbb  182  syl5bbr  183  3bitr4g  212  imim21b  241  pm5.17dc  798  dn1dc  853  bilukdc  1268  nf4dc  1538  sbal1  1856  abbi  2129  necon3abid  2218  necon3bid  2220  necon1abiidc  2239  r19.21t  2368  ceqsralt  2554  ceqsrexv  2647  ceqsrex2v  2649  elab2g  2662  elrabf  2669  eueq2dc  2687  euxfrdc  2700  eqreu  2706  reu8  2710  ru  2736  sbcralt  2807  sbcrext  2808  sbcne12g  2841  csbnestgf  2871  disjpss  3251  ralprg  3391  rexprg  3392  difsn  3471  opthpr  3513  ralunsn  3538  dfiin2g  3660  iunxsng  3702  elpwuni  3711  pwnss  3882  opelopabt  3969  opelopabga  3970  brabga  3971  elsucg  4086  elsuc2g  4087  brab2a  4316  opeliunxp  4318  posng  4335  brab2ga  4338  csbdmg  4452  elrnmpt1  4508  elrnmptg  4509  poleloe  4647  elxp4  4731  elxp5  4732  cnvpom  4783  sbcfung  4847  dffun8  4851  fncnv  4887  fununi  4889  fnssresb  4933  fnimaeq0  4942  funcocnv2  5072  dffn5im  5140  funimass4  5145  fnsnfv  5153  dmfco  5162  fndmdif  5193  fndmin  5195  unpreima  5213  respreima  5216  fsn2  5258  fnressn  5270  fressnfv  5271  elunirn  5326  dff13  5328  fliftel  5354  isoini  5378  f1oiso  5386  acexmid  5431  eloprabga  5510  resoprab2  5517  ralrnmpt2  5534  rexrnmpt2  5535  ovid  5536  ov  5539  ovg  5558  ofrfval2  5646  fmpt2x  5745  1stconst  5761  2ndconst  5762  isprmpt2  5776  brtpos2  5784  dfsmo2  5820  brdifun  6040  eqerlem  6044  brecop  6103  erovlem  6105  ltpiord  6173  nlt1pig  6195  elinp  6322  ltdfpr  6354  genpassl  6373  genpassu  6374  1idprl  6423  1idpru  6424  gt0srpr  6489  axprecex  6568  xrlenlt  6679  addsubeq4  6813  renegcl  6858  bj-indeq  7291  bj-nn0sucALT  7335
  Copyright terms: Public domain W3C validator