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

Theorem imbi2d 228
Description: Deduction adding an antecedent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
imbid.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
imbi2d  |-  ( ph  ->  ( ( th  ->  ps )  <->  ( th  ->  ch ) ) )

Proof of Theorem imbi2d
StepHypRef Expression
1 imbid.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21a1d 22 . 2  |-  ( ph  ->  ( th  ->  ( ps 
<->  ch ) ) )
32pm5.74d 180 1  |-  ( ph  ->  ( ( th  ->  ps )  <->  ( th  ->  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  imbi12d  232  imbi2  235  pm5.42  313  imanst  777  imandc  822  pm4.14dc  823  imimorbdc  831  pm5.6dc  871  ax11v2  1745  ax11v  1752  equs5or  1755  mo23  1986  2gencl  2646  3gencl  2647  vtocl2gf  2674  vtocl3gf  2675  eqeu  2776  mo2icl  2785  euind  2793  reu7  2801  reuind  2809  sbctt  2894  sbcnestgf  2968  preq12bg  3600  elint  3677  elintrabg  3684  intab  3700  trss  3920  bm1.3ii  3935  pocl  4104  swopolem  4106  sowlin  4121  frforeq3  4148  frirrg  4151  frind  4153  reusv3  4256  regexmid  4324  ordsoexmid  4351  tfisi  4375  finds2  4389  nnregexmid  4407  vtoclr  4454  2optocl  4483  3optocl  4484  raliunxp  4545  resieq  4691  iss  4725  cnveqb  4852  funmo  4996  fnbrfvb  5308  fvelimab  5323  fvmptssdm  5350  fmptco  5427  fnressn  5446  fressnfv  5447  isoselem  5560  isosolem  5564  ovg  5740  caovcan  5766  caovordig  5767  caovord  5773  f1o2ndf1  5950  poxp  5954  smoeq  6009  smores  6011  tfrlem1  6027  tfrlemi1  6051  tfrexlem  6053  tfri3  6086  oawordriexmid  6185  nnacl  6195  nnmcl  6196  nnacom  6199  nnaass  6200  nndi  6201  nnmass  6202  nnmsucr  6203  nnmcom  6204  nnsucsssuc  6207  nntri3or  6208  nnaordi  6219  nnaword  6222  nnmordi  6227  nnaordex  6238  2ecoptocl  6332  3ecoptocl  6333  th3qlem2  6347  xpdom2g  6500  findcard2  6557  findcard2s  6558  xpfi  6590  supeq1  6625  ordiso2  6672  updjud  6717  distrnq0  6962  addassnq0  6965  elinp  6977  prcdnql  6987  prcunqu  6988  prarloclem3  7000  caucvgpr  7185  caucvgprpr  7215  ltsosr  7254  caucvgsrlemcau  7282  caucvgsrlemgt1  7284  caucvgsrlemoffres  7289  pitonn  7329  axpre-ltwlin  7362  axcaucvglemres  7378  nnaddcl  8377  nnmulcl  8378  zaddcllempos  8720  zaddcllemneg  8722  prime  8778  peano5uzti  8787  uzind2  8791  zindd  8797  uzaddcl  9006  exfzdc  9579  frec2uzltd  9738  frec2uzrdg  9744  frecuzrdgtcl  9747  frecuzrdgg  9751  frecuzrdgfunlem  9754  iseqvalt  9790  iseqclt  9798  iseqoveq  9799  iseqss  9800  iseqsst  9801  iseqfveq2  9803  iseqshft2  9807  monoord  9810  iseqsplit  9813  iseqcaopr3  9815  iseqf1olemp  9836  iseqid3s  9842  iseqid2  9844  iseqhomo  9845  iseqz  9846  expivallem  9855  expcllem  9865  expap0  9884  mulexp  9893  expadd  9896  expmul  9899  leexp2r  9908  leexp1a  9909  bernneq  9971  facdiv  10043  faclbnd  10046  faclbnd6  10049  omgadd  10107  iseqcoll  10144  shftvalg  10167  shftval4g  10168  cjexp  10223  resqrexlemover  10339  resqrexlemdecn  10341  resqrexlemlo  10342  resqrexlemcalc3  10345  absexp  10408  climshft  10587  climub  10626  climserile  10627  dvdsfac  10743  infssuzex  10827  bezoutlemstep  10868  bezoutlemmain  10869  bezoutlemex  10872  dfgcd2  10885  gcdmultiple  10891  rplpwr  10898  nn0seqcvgd  10905  ialginv  10911  ialgcvga  10915  ialgfx  10916  isprm4  10983  prmind2  10984  prmdvdsexp  11009  prmfac1  11013  bdbm1.3ii  11227  bj-2inf  11278  bj-omtrans  11296  nninfalllemn  11343  nninfalllem1  11344  nninfsellemdc  11347  nninfsellemqall  11352
  Copyright terms: Public domain W3C validator