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  794  dn1dc  851  bilukdc  1268  nf4dc  1536  sbal1  1854  abbi  2127  necon3abid  2216  necon3bid  2218  necon1abiidc  2237  r19.21t  2366  ceqsralt  2552  ceqsrexv  2645  ceqsrex2v  2647  elab2g  2660  elrabf  2667  eueq2dc  2685  euxfrdc  2698  eqreu  2704  reu8  2708  ru  2734  sbcralt  2805  sbcrext  2806  sbcne12g  2839  csbnestgf  2869  disjpss  3249  ralprg  3387  rexprg  3388  difsn  3467  opthpr  3509  ralunsn  3534  dfiin2g  3656  iunxsng  3698  elpwuni  3707  pwnss  3878  opelopabt  3965  opelopabga  3966  brabga  3967  elsucg  4082  elsuc2g  4083  brab2a  4311  opeliunxp  4313  posng  4330  brab2ga  4333  csbdmg  4447  elrnmpt1  4503  elrnmptg  4504  poleloe  4642  elxp4  4726  elxp5  4727  cnvpom  4778  sbcfung  4842  dffun8  4846  fncnv  4882  fununi  4884  fnssresb  4928  fnimaeq0  4937  funcocnv2  5067  dffn5im  5135  funimass4  5140  fnsnfv  5148  dmfco  5157  fndmdif  5188  fndmin  5190  unpreima  5208  respreima  5211  fsn2  5253  fnressn  5265  fressnfv  5266  elunirn  5321  dff13  5323  fliftel  5349  isoini  5373  f1oiso  5381  acexmid  5426  eloprabga  5505  resoprab2  5512  ralrnmpt2  5529  rexrnmpt2  5530  ovid  5531  ov  5534  ovg  5553  ofrfval2  5641  fmpt2x  5740  1stconst  5756  2ndconst  5757  isprmpt2  5771  brtpos2  5779  dfsmo2  5815  brdifun  6035  eqerlem  6039  brecop  6098  erovlem  6100  ltpiord  6168  nlt1pig  6190  elinp  6317  ltdfpr  6349  genpassl  6368  genpassu  6369  1idprl  6418  1idpru  6419  gt0srpr  6489  axprecex  6572  xrlenlt  6687  addsubeq4  6829  renegcl  6874  lesub0  7075  recexaplem2  7221  conjmulap  7293  rerecclap  7294  creui  7498  peano2nn  7512  nndiv  7540  elznn0  7837  ltxr  8174  divelunit  8349  iccf1o  8351  bj-indeq  8506  bj-nn0sucALT  8550
  Copyright terms: Public domain W3C validator