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  imandc  820  pm4.14dc  821  imimorbdc  829  pm5.6dc  869  ax11v2  1742  ax11v  1749  equs5or  1752  mo23  1983  2gencl  2633  3gencl  2634  vtocl2gf  2661  vtocl3gf  2662  eqeu  2763  mo2icl  2772  euind  2780  reu7  2788  reuind  2796  sbctt  2881  sbcnestgf  2954  preq12bg  3573  elint  3650  elintrabg  3657  intab  3673  trss  3892  bm1.3ii  3907  pocl  4066  swopolem  4068  sowlin  4083  frforeq3  4110  frirrg  4113  frind  4115  reusv3  4218  regexmid  4286  ordsoexmid  4313  tfisi  4336  finds2  4350  nnregexmid  4368  vtoclr  4414  2optocl  4443  3optocl  4444  raliunxp  4505  resieq  4650  iss  4684  cnveqb  4806  funmo  4947  fnbrfvb  5246  fvelimab  5261  fvmptssdm  5287  fmptco  5362  fnressn  5381  fressnfv  5382  isoselem  5490  isosolem  5494  ovg  5670  caovcan  5696  caovordig  5697  caovord  5703  f1o2ndf1  5880  poxp  5884  smoeq  5939  smores  5941  tfrlem1  5957  tfrlemi1  5981  tfrexlem  5983  tfri3  6016  oawordriexmid  6114  nnacl  6124  nnmcl  6125  nnacom  6128  nnaass  6129  nndi  6130  nnmass  6131  nnmsucr  6132  nnmcom  6133  nnsucsssuc  6136  nntri3or  6137  nnaordi  6147  nnaword  6150  nnmordi  6155  nnaordex  6166  2ecoptocl  6260  3ecoptocl  6261  th3qlem2  6275  xpdom2g  6376  findcard2  6423  findcard2s  6424  supeq1  6458  ordiso2  6505  distrnq0  6711  addassnq0  6714  elinp  6726  prcdnql  6736  prcunqu  6737  prarloclem3  6749  caucvgpr  6934  caucvgprpr  6964  ltsosr  7003  caucvgsrlemcau  7031  caucvgsrlemgt1  7033  caucvgsrlemoffres  7038  pitonn  7078  axpre-ltwlin  7111  axcaucvglemres  7127  nnaddcl  8126  nnmulcl  8127  zaddcllempos  8469  zaddcllemneg  8471  prime  8527  peano5uzti  8536  uzind2  8540  zindd  8546  uzaddcl  8755  exfzdc  9326  frec2uzltd  9485  frec2uzrdg  9491  frecuzrdgtcl  9494  frecuzrdgg  9498  frecuzrdgfunlem  9501  iseqvalt  9532  iseqoveq  9540  iseqss  9541  iseqsst  9542  iseqfveq2  9544  iseqshft2  9548  monoord  9551  iseqsplit  9554  iseqcaopr3  9556  iseqid3s  9562  iseqid2  9564  iseqhomo  9565  iseqz  9566  expivallem  9574  expcllem  9584  expap0  9603  mulexp  9612  expadd  9615  expmul  9618  leexp2r  9627  leexp1a  9628  bernneq  9690  facdiv  9762  faclbnd  9765  faclbnd6  9768  omgadd  9826  shftvalg  9862  shftval4g  9863  cjexp  9918  resqrexlemover  10034  resqrexlemdecn  10036  resqrexlemlo  10037  resqrexlemcalc3  10040  absexp  10103  climshft  10281  climub  10320  climserile  10321  dvdsfac  10405  infssuzex  10489  bezoutlemstep  10530  bezoutlemmain  10531  bezoutlemex  10534  dfgcd2  10547  gcdmultiple  10553  rplpwr  10560  nn0seqcvgd  10567  ialginv  10573  ialgcvga  10577  ialgfx  10578  isprm4  10645  prmind2  10646  prmdvdsexp  10671  prmfac1  10675  bdbm1.3ii  10840  bj-2inf  10891  bj-omtrans  10909
  Copyright terms: Public domain W3C validator