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  809  dn1dc  866  bilukdc  1284  nf4dc  1557  sbal1  1875  abbi  2148  necon3abid  2238  necon3bid  2240  necon1abiidc  2259  r19.21t  2388  ceqsralt  2575  ceqsrexv  2668  ceqsrex2v  2670  elab2g  2683  elrabf  2690  eueq2dc  2708  euxfrdc  2721  eqreu  2727  reu8  2731  ru  2757  sbcralt  2828  sbcrext  2829  sbcne12g  2862  csbnestgf  2892  disjpss  3272  ralprg  3412  rexprg  3413  difsn  3492  opthpr  3534  ralunsn  3559  dfiin2g  3681  iunxsng  3723  elpwuni  3732  pwnss  3903  opelopabt  3990  opelopabga  3991  brabga  3992  elsucg  4107  elsuc2g  4108  brab2a  4336  opeliunxp  4338  posng  4355  brab2ga  4358  csbdmg  4472  elrnmpt1  4528  elrnmptg  4529  poleloe  4667  elxp4  4751  elxp5  4752  cnvpom  4803  sbcfung  4868  dffun8  4872  fncnv  4908  fununi  4910  fnssresb  4954  fnimaeq0  4963  funcocnv2  5094  dffn5im  5162  funimass4  5167  fnsnfv  5175  dmfco  5184  fndmdif  5215  fndmin  5217  unpreima  5235  respreima  5238  fsn2  5280  fnressn  5292  fressnfv  5293  elunirn  5348  dff13  5350  fliftel  5376  isoini  5400  f1oiso  5408  acexmid  5454  eloprabga  5533  resoprab2  5540  ralrnmpt2  5557  rexrnmpt2  5558  ovid  5559  ov  5562  ovg  5581  ofrfval2  5669  fmpt2x  5768  1stconst  5784  2ndconst  5785  isprmpt2  5799  brtpos2  5807  dfsmo2  5843  brdifun  6069  eqerlem  6073  brecop  6132  erovlem  6134  xpsnen  6231  xpdom2  6241  ltpiord  6303  nlt1pig  6325  elinp  6456  ltdfpr  6488  genpassl  6507  genpassu  6508  1idprl  6564  1idpru  6565  gt0srpr  6636  axprecex  6724  xrlenlt  6841  addsubeq4  6983  renegcl  7028  lesub0  7229  recexaplem2  7375  conjmulap  7447  rerecclap  7448  creui  7653  peano2nn  7667  nndiv  7695  elznn0  7996  eqreznegel  8285  ltxr  8425  divelunit  8600  iccf1o  8602  elfz2  8611  elfzp1  8664  fzdifsuc  8673  fznn  8681  fzosplitsni  8821  frec2uzisod  8834  sq11i  8956  cjreb  9054  bj-indeq  9318  bj-nn0sucALT  9362
  Copyright terms: Public domain W3C validator