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

Theorem biimtrid 152
Description: A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded antecedent with a definition. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
biimtrid.1 (𝜑𝜓)
biimtrid.2 (𝜒 → (𝜓𝜃))
Assertion
Ref Expression
biimtrid (𝜒 → (𝜑𝜃))

Proof of Theorem biimtrid
StepHypRef Expression
1 biimtrid.1 . . 3 (𝜑𝜓)
21biimpi 120 . 2 (𝜑𝜓)
3 biimtrid.2 . 2 (𝜒 → (𝜓𝜃))
42, 3syl5 32 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
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  3imtr4g  205  ancomsd  269  pm2.13dc  885  3jao  1301  19.33b2  1629  sbequ2  1769  sbi1v  1891  mor  2068  2euex  2113  eqneqall  2357  necon3ad  2389  necon1aidc  2398  necon4addc  2417  elnelall  2454  spcimgft  2813  spcimegft  2815  rspc  2835  rspcimdv  2842  rspc2gv  2853  euind  2924  2reuswapdc  2941  reuind  2942  sbciegft  2993  rspsbc  3045  preqr2g  3765  prel12  3769  intss1  3857  intmin  3862  iinss  3935  disjiun  3995  trel3  4106  trin  4108  repizf2  4159  exmidsssnc  4200  copsexg  4241  po3nr  4307  sowlin  4317  eusvnfb  4451  reusv3  4457  ssorduni  4483  ordsucim  4496  tfis2f  4580  ssrelrel  4723  relop  4773  iss  4949  poirr2  5017  funopg  5246  funssres  5254  funun  5256  funcnvuni  5281  fv3  5534  fvmptt  5603  dff4im  5658  f1eqcocnv  5786  oprabid  5901  f1o2ndf1  6223  poxp  6227  reldmtpos  6248  rntpos  6252  smoiun  6296  tfrlem1  6303  tfrlemi1  6327  tfrexlem  6329  tfri3  6362  nntri3or  6488  qsss  6588  th3qlem1  6631  ixpsnf1o  6730  phplem4  6849  fimax2gtri  6895  fiintim  6922  fisseneq  6925  sbthlemi10  6959  supmoti  6986  suplub2ti  6994  ordiso2  7028  ltmpig  7329  prcdnql  7474  prcunqu  7475  recexprlem1ssl  7623  recexprlem1ssu  7624  recexprlemss1l  7625  recexprlemss1u  7626  cauappcvgprlemladdru  7646  cauappcvgprlemladdrl  7647  caucvgprlemladdrl  7668  mulgt0sr  7768  suplocsrlem  7798  axprecex  7870  ltxrlt  8013  addid0  8320  negf1o  8329  cju  8907  nngt1ne1  8943  nnsub  8947  0mnnnnn0  9197  un0addcl  9198  un0mulcl  9199  zapne  9316  eluzuzle  9525  indstr  9582  elpq  9637  xposdif  9869  ixxdisj  9890  icodisj  9979  uzsubsubfz  10033  elfzmlbp  10118  fzofzim  10174  subfzo0  10228  addmodlteq  10384  seq3f1olemp  10488  expcl2lemap  10518  expnegzap  10540  expaddzap  10550  expmulzap  10552  facwordi  10704  bccl  10731  hashfacen  10800  ovshftex  10812  cau3lem  11107  maxabslemval  11201  rexanre  11213  xrmaxiflemval  11242  2clim  11293  summodc  11375  fsum2dlemstep  11426  fsumiun  11469  prodmodc  11570  fprod2dlemstep  11614  odd2np1lem  11860  oddge22np1  11869  sqoddm1div8z  11874  divalglemeunn  11909  divalglemeuneg  11911  gcd0id  11963  divgcdcoprm0  12084  prmdvdsexpr  12133  prmfac1  12135  qnumdencl  12170  hashdvds  12204  prm23lt5  12246  pcneg  12307  prmpwdvds  12336  ctinf  12414  mnd1id  12738  0subm  12761  insubm  12762  dfgrp3mlem  12857  tgcl  13231  epttop  13257  txbas  13425  txbasval  13434  txcnp  13438  txdis1cn  13445  bldisj  13568  reopnap  13705  dvfgg  13824  lgsdir2lem2  14097  bj-vtoclgft  14183  bj-charfun  14215  bj-charfunbi  14219  bj-indind  14340  bj-nntrans  14359  bj-nnelirr  14361  triap  14433
  Copyright terms: Public domain W3C validator