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

Theorem bitrid 192
Description: A syllogism inference from two biconditionals. (Contributed by NM, 12-Mar-1993.)
Hypotheses
Ref Expression
bitrid.1 (𝜑𝜓)
bitrid.2 (𝜒 → (𝜓𝜃))
Assertion
Ref Expression
bitrid (𝜒 → (𝜑𝜃))

Proof of Theorem bitrid
StepHypRef Expression
1 bitrid.1 . . 3 (𝜑𝜓)
21a1i 9 . 2 (𝜒 → (𝜑𝜓))
3 bitrid.2 . 2 (𝜒 → (𝜓𝜃))
42, 3bitrd 188 1 (𝜒 → (𝜑𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  bitr2id  193  bitr3id  194  3bitr4g  223  imim21b  253  pm5.17dc  904  dn1dc  960  bilukdc  1396  nf4dc  1670  sbal1  2002  abbi  2291  necon3abid  2386  necon3bid  2388  necon1abiidc  2407  r19.21t  2552  ceqsralt  2764  ceqsrexv  2867  ceqsrex2v  2869  elab2g  2884  elrabf  2891  eueq2dc  2910  euxfrdc  2923  eqreu  2929  reu8  2933  ru  2961  sbcralt  3039  sbcrext  3040  sbcne12g  3075  csbnestgf  3109  dfss4st  3368  rexsng  3632  ralprg  3642  rexprg  3643  difsn  3728  opthpr  3770  ralunsn  3795  dfiin2g  3917  iunxsng  3959  iunxsngf  3961  elpwuni  3973  pwnss  4156  exmid01  4195  opelopabt  4259  opelopabga  4260  brabga  4261  elsucg  4401  elsuc2g  4402  brab2a  4676  opeliunxp  4678  posng  4695  brab2ga  4698  csbdmg  4817  elrnmpt1  4874  elrnmptg  4875  eliniseg2  5004  poleloe  5024  elxp4  5112  elxp5  5113  cnvpom  5167  sbcfung  5236  dffun8  5240  fncnv  5278  fununi  5280  fnssresb  5324  fnimaeq0  5333  funcocnv2  5482  dffn5im  5557  funimass4  5562  fnsnfv  5571  dmfco  5580  fndmdif  5617  fndmin  5619  unpreima  5637  respreima  5640  fsn2  5686  fnressn  5698  fressnfv  5699  elunirn  5761  dff13  5763  fliftel  5788  isoini  5813  f1oiso  5821  acexmid  5868  eloprabga  5956  resoprab2  5966  ralrnmpo  5983  rexrnmpo  5984  ovid  5985  ov  5988  ovg  6007  ofrfval2  6093  fmpox  6195  1stconst  6216  2ndconst  6217  f1od2  6230  rbropapd  6237  brtpos2  6246  dfsmo2  6282  frecabcl  6394  brdifun  6556  eqerlem  6560  brecop  6619  erovlem  6621  mapsn  6684  mptelixpg  6728  map1  6806  xpsnen  6815  xpdom2  6825  xpf1o  6838  supubti  6992  infglbti  7018  ctssdccl  7104  nninfwlpoim  7170  netap  7244  2omotaplemap  7247  ltpiord  7309  nlt1pig  7331  elinp  7464  ltdfpr  7496  genpassl  7514  genpassu  7515  1idprl  7580  1idpru  7581  gt0srpr  7738  mappsrprg  7794  map2psrprg  7795  peano2nnnn  7843  recidpirq  7848  axprecex  7870  xrlenlt  8012  addsubeq4  8162  renegcl  8208  lesub0  8426  recexaplem2  8598  conjmulap  8675  rerecclap  8676  creui  8906  peano2nn  8920  nndiv  8949  elznn0  9257  eqreznegel  9603  negelrp  9674  ltxr  9762  divelunit  9989  iccf1o  9991  elfz2  10002  elfzp1  10058  fzdifsuc  10067  fznn  10075  fzosplitsni  10221  fvinim0ffz  10227  frec2uzisod  10393  sq11i  10595  cjreb  10859  rexfiuz  10982  cau3lem  11107  pwm1geoserap1  11500  mertensabs  11529  divides  11780  dvdsabseq  11836  odd2np1  11861  oddm1even  11863  modremain  11917  infssuzex  11933  zsupssdc  11938  bezoutlemnewy  11980  bezoutlemstep  11981  bezoutlemmain  11982  bezoutlema  11983  bezoutlemb  11984  isprm2  12100  isprm4  12102  dvdsnprmd  12108  oddprmdvds  12335  4sqlem2  12370  issubm  12753  grplmulf1o  12833  grplactcnv  12861  srg1zr  12996  iscrng2  13024  istopg  13164  basgen2  13248  isnei  13311  restdis  13351  iscn  13364  iscnp  13366  lmbr2  13381  lmbrf  13382  txcn  13442  cnmpt21  13458  blres  13601  isxms2  13619  metrest  13673  metcnp  13679  txmetcnp  13685  txmetcn  13686  cnblcld  13702  reopnap  13705  ioocosf1o  13942  bj-nn0sucALT  14386  apdiff  14452
  Copyright terms: Public domain W3C validator