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

Theorem syl5bb 191
 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 187 1 (𝜒 → (𝜑𝜃))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  syl5rbb  192  bitr3id  193  3bitr4g  222  imim21b  251  pm5.17dc  890  dn1dc  945  bilukdc  1375  nf4dc  1649  sbal1  1978  abbi  2254  necon3abid  2348  necon3bid  2350  necon1abiidc  2369  r19.21t  2510  ceqsralt  2716  ceqsrexv  2818  ceqsrex2v  2820  elab2g  2834  elrabf  2841  eueq2dc  2860  euxfrdc  2873  eqreu  2879  reu8  2883  ru  2911  sbcralt  2988  sbcrext  2989  sbcne12g  3024  csbnestgf  3056  dfss4st  3313  rexsng  3571  ralprg  3581  rexprg  3582  difsn  3664  opthpr  3706  ralunsn  3731  dfiin2g  3853  iunxsng  3895  iunxsngf  3897  elpwuni  3909  pwnss  4090  exmid01  4128  opelopabt  4191  opelopabga  4192  brabga  4193  elsucg  4333  elsuc2g  4334  brab2a  4599  opeliunxp  4601  posng  4618  brab2ga  4621  csbdmg  4740  elrnmpt1  4797  elrnmptg  4798  poleloe  4945  elxp4  5033  elxp5  5034  cnvpom  5088  sbcfung  5154  dffun8  5158  fncnv  5196  fununi  5198  fnssresb  5242  fnimaeq0  5251  funcocnv2  5399  dffn5im  5474  funimass4  5479  fnsnfv  5487  dmfco  5496  fndmdif  5532  fndmin  5534  unpreima  5552  respreima  5555  fsn2  5601  fnressn  5613  fressnfv  5614  elunirn  5674  dff13  5676  fliftel  5701  isoini  5726  f1oiso  5734  acexmid  5780  eloprabga  5865  resoprab2  5875  ralrnmpo  5892  rexrnmpo  5893  ovid  5894  ov  5897  ovg  5916  ofrfval2  6005  fmpox  6105  1stconst  6125  2ndconst  6126  f1od2  6139  rbropapd  6146  brtpos2  6155  dfsmo2  6191  frecabcl  6303  brdifun  6463  eqerlem  6467  brecop  6526  erovlem  6528  mapsn  6591  mptelixpg  6635  map1  6713  xpsnen  6722  xpdom2  6732  xpf1o  6745  supubti  6893  infglbti  6919  ctssdccl  7003  ltpiord  7150  nlt1pig  7172  elinp  7305  ltdfpr  7337  genpassl  7355  genpassu  7356  1idprl  7421  1idpru  7422  gt0srpr  7579  mappsrprg  7635  map2psrprg  7636  peano2nnnn  7684  recidpirq  7689  axprecex  7711  xrlenlt  7852  addsubeq4  8000  renegcl  8046  lesub0  8264  recexaplem2  8436  conjmulap  8512  rerecclap  8513  creui  8741  peano2nn  8755  nndiv  8784  elznn0  9092  eqreznegel  9432  negelrp  9503  ltxr  9591  divelunit  9814  iccf1o  9816  elfz2  9827  elfzp1  9882  fzdifsuc  9891  fznn  9899  fzosplitsni  10042  fvinim0ffz  10048  frec2uzisod  10210  sq11i  10412  cjreb  10669  rexfiuz  10792  cau3lem  10917  pwm1geoserap1  11308  mertensabs  11337  divides  11529  dvdsabseq  11579  odd2np1  11604  oddm1even  11606  modremain  11660  infssuzex  11676  bezoutlemnewy  11718  bezoutlemstep  11719  bezoutlemmain  11720  bezoutlema  11721  bezoutlemb  11722  isprm2  11832  isprm4  11834  dvdsnprmd  11840  istopg  12203  basgen2  12287  isnei  12350  restdis  12390  iscn  12403  iscnp  12405  lmbr2  12420  lmbrf  12421  txcn  12481  cnmpt21  12497  blres  12640  isxms2  12658  metrest  12712  metcnp  12718  txmetcnp  12724  txmetcn  12725  cnblcld  12741  reopnap  12744  ioocosf1o  12981  bj-indeq  13296  bj-nn0sucALT  13345  apdiff  13414
 Copyright terms: Public domain W3C validator