ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  biimtrid Unicode 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  |-  ( ph  <->  ps )
biimtrid.2  |-  ( ch 
->  ( ps  ->  th )
)
Assertion
Ref Expression
biimtrid  |-  ( ch 
->  ( ph  ->  th )
)

Proof of Theorem biimtrid
StepHypRef Expression
1 biimtrid.1 . . 3  |-  ( ph  <->  ps )
21biimpi 120 . 2  |-  ( ph  ->  ps )
3 biimtrid.2 . 2  |-  ( ch 
->  ( ps  ->  th )
)
42, 3syl5 32 1  |-  ( ch 
->  ( ph  ->  th )
)
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  4240  po3nr  4306  sowlin  4316  eusvnfb  4450  reusv3  4456  ssorduni  4482  ordsucim  4495  tfis2f  4579  ssrelrel  4722  relop  4772  iss  4948  poirr2  5016  funopg  5245  funssres  5253  funun  5255  funcnvuni  5280  fv3  5533  fvmptt  5602  dff4im  5657  f1eqcocnv  5785  oprabid  5900  f1o2ndf1  6222  poxp  6226  reldmtpos  6247  rntpos  6251  smoiun  6295  tfrlem1  6302  tfrlemi1  6326  tfrexlem  6328  tfri3  6361  nntri3or  6487  qsss  6587  th3qlem1  6630  ixpsnf1o  6729  phplem4  6848  fimax2gtri  6894  fiintim  6921  fisseneq  6924  sbthlemi10  6958  supmoti  6985  suplub2ti  6993  ordiso2  7027  ltmpig  7316  prcdnql  7461  prcunqu  7462  recexprlem1ssl  7610  recexprlem1ssu  7611  recexprlemss1l  7612  recexprlemss1u  7613  cauappcvgprlemladdru  7633  cauappcvgprlemladdrl  7634  caucvgprlemladdrl  7655  mulgt0sr  7755  suplocsrlem  7785  axprecex  7857  ltxrlt  8000  addid0  8307  negf1o  8316  cju  8894  nngt1ne1  8930  nnsub  8934  0mnnnnn0  9184  un0addcl  9185  un0mulcl  9186  zapne  9303  eluzuzle  9512  indstr  9569  elpq  9624  xposdif  9856  ixxdisj  9877  icodisj  9966  uzsubsubfz  10020  elfzmlbp  10105  fzofzim  10161  subfzo0  10215  addmodlteq  10371  seq3f1olemp  10475  expcl2lemap  10505  expnegzap  10527  expaddzap  10537  expmulzap  10539  facwordi  10691  bccl  10718  hashfacen  10787  ovshftex  10799  cau3lem  11094  maxabslemval  11188  rexanre  11200  xrmaxiflemval  11229  2clim  11280  summodc  11362  fsum2dlemstep  11413  fsumiun  11456  prodmodc  11557  fprod2dlemstep  11601  odd2np1lem  11847  oddge22np1  11856  sqoddm1div8z  11861  divalglemeunn  11896  divalglemeuneg  11898  gcd0id  11950  divgcdcoprm0  12071  prmdvdsexpr  12120  prmfac1  12122  qnumdencl  12157  hashdvds  12191  prm23lt5  12233  pcneg  12294  prmpwdvds  12323  ctinf  12401  mnd1id  12725  0subm  12748  insubm  12749  dfgrp3mlem  12844  tgcl  13197  epttop  13223  txbas  13391  txbasval  13400  txcnp  13404  txdis1cn  13411  bldisj  13534  reopnap  13671  dvfgg  13790  lgsdir2lem2  14063  bj-vtoclgft  14149  bj-charfun  14181  bj-charfunbi  14185  bj-indind  14306  bj-nntrans  14325  bj-nnelirr  14327  triap  14400
  Copyright terms: Public domain W3C validator