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

Theorem syl5bb 185
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl5bb.1  |-  ( ph  <->  ps )
syl5bb.2  |-  ( ch 
->  ( ps  <->  th )
)
Assertion
Ref Expression
syl5bb  |-  ( ch 
->  ( ph  <->  th )
)

Proof of Theorem syl5bb
StepHypRef Expression
1 syl5bb.1 . . 3  |-  ( ph  <->  ps )
21a1i 9 . 2  |-  ( ch 
->  ( ph  <->  ps )
)
3 syl5bb.2 . 2  |-  ( ch 
->  ( ps  <->  th )
)
42, 3bitrd 181 1  |-  ( ch 
->  ( ph  <->  th )
)
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:  syl5rbb  186  syl5bbr  187  3bitr4g  216  imim21b  245  pm5.17dc  821  dn1dc  878  bilukdc  1303  nf4dc  1576  sbal1  1894  abbi  2167  necon3abid  2259  necon3bid  2261  necon1abiidc  2280  r19.21t  2411  ceqsralt  2598  ceqsrexv  2697  ceqsrex2v  2699  elab2g  2712  elrabf  2719  eueq2dc  2737  euxfrdc  2750  eqreu  2756  reu8  2760  ru  2786  sbcralt  2862  sbcrext  2863  sbcne12g  2896  csbnestgf  2926  disjpss  3306  ralprg  3449  rexprg  3450  difsn  3529  opthpr  3571  ralunsn  3596  dfiin2g  3718  iunxsng  3760  elpwuni  3769  pwnss  3940  opelopabt  4027  opelopabga  4028  brabga  4029  elsucg  4169  elsuc2g  4170  brab2a  4421  opeliunxp  4423  posng  4440  brab2ga  4443  csbdmg  4557  elrnmpt1  4613  elrnmptg  4614  poleloe  4752  elxp4  4836  elxp5  4837  cnvpom  4888  sbcfung  4953  dffun8  4957  fncnv  4993  fununi  4995  fnssresb  5039  fnimaeq0  5048  funcocnv2  5179  dffn5im  5247  funimass4  5252  fnsnfv  5260  dmfco  5269  fndmdif  5300  fndmin  5302  unpreima  5320  respreima  5323  fsn2  5365  fnressn  5377  fressnfv  5378  elunirn  5433  dff13  5435  fliftel  5461  isoini  5485  f1oiso  5493  acexmid  5539  eloprabga  5619  resoprab2  5626  ralrnmpt2  5643  rexrnmpt2  5644  ovid  5645  ov  5648  ovg  5667  ofrfval2  5755  fmpt2x  5854  1stconst  5870  2ndconst  5871  f1od2  5884  isprmpt2  5889  brtpos2  5897  dfsmo2  5933  brdifun  6164  eqerlem  6168  brecop  6227  erovlem  6229  xpsnen  6326  xpdom2  6336  supubti  6405  ltpiord  6475  nlt1pig  6497  elinp  6630  ltdfpr  6662  genpassl  6680  genpassu  6681  1idprl  6746  1idpru  6747  gt0srpr  6891  peano2nnnn  6987  recidpirq  6992  axprecex  7012  xrlenlt  7143  addsubeq4  7289  renegcl  7335  lesub0  7548  recexaplem2  7707  conjmulap  7780  rerecclap  7781  creui  7988  peano2nn  8002  nndiv  8030  elznn0  8317  eqreznegel  8646  ltxr  8796  divelunit  8971  iccf1o  8973  elfz2  8983  elfzp1  9036  fzdifsuc  9045  fznn  9053  fzosplitsni  9193  fvinim0ffz  9198  frec2uzisod  9357  sq11i  9509  cjreb  9694  rexfiuz  9816  cau3lem  9941  divides  10110  dvdsabseq  10159  odd2np1  10184  oddm1even  10186  modremain  10241  bj-indeq  10440  bj-nn0sucALT  10490
  Copyright terms: Public domain W3C validator