ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  imbi2d GIF 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 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
imbi2d (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))

Proof of Theorem imbi2d
StepHypRef Expression
1 imbid.1 . . 3 (𝜑 → (𝜓𝜒))
21a1d 22 . 2 (𝜑 → (𝜃 → (𝜓𝜒)))
32pm5.74d 180 1 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
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  3919  bm1.3ii  3934  pocl  4103  swopolem  4105  sowlin  4120  frforeq3  4147  frirrg  4150  frind  4152  reusv3  4255  regexmid  4323  ordsoexmid  4350  tfisi  4374  finds2  4388  nnregexmid  4406  vtoclr  4453  2optocl  4482  3optocl  4483  raliunxp  4544  resieq  4690  iss  4724  cnveqb  4849  funmo  4993  fnbrfvb  5302  fvelimab  5317  fvmptssdm  5344  fmptco  5421  fnressn  5440  fressnfv  5441  isoselem  5554  isosolem  5558  ovg  5734  caovcan  5760  caovordig  5761  caovord  5767  f1o2ndf1  5944  poxp  5948  smoeq  6003  smores  6005  tfrlem1  6021  tfrlemi1  6045  tfrexlem  6047  tfri3  6080  oawordriexmid  6179  nnacl  6189  nnmcl  6190  nnacom  6193  nnaass  6194  nndi  6195  nnmass  6196  nnmsucr  6197  nnmcom  6198  nnsucsssuc  6201  nntri3or  6202  nnaordi  6213  nnaword  6216  nnmordi  6221  nnaordex  6232  2ecoptocl  6326  3ecoptocl  6327  th3qlem2  6341  xpdom2g  6494  findcard2  6551  findcard2s  6552  xpfi  6584  supeq1  6618  ordiso2  6665  updjud  6710  distrnq0  6955  addassnq0  6958  elinp  6970  prcdnql  6980  prcunqu  6981  prarloclem3  6993  caucvgpr  7178  caucvgprpr  7208  ltsosr  7247  caucvgsrlemcau  7275  caucvgsrlemgt1  7277  caucvgsrlemoffres  7282  pitonn  7322  axpre-ltwlin  7355  axcaucvglemres  7371  nnaddcl  8370  nnmulcl  8371  zaddcllempos  8713  zaddcllemneg  8715  prime  8771  peano5uzti  8780  uzind2  8784  zindd  8790  uzaddcl  8999  exfzdc  9572  frec2uzltd  9731  frec2uzrdg  9737  frecuzrdgtcl  9740  frecuzrdgg  9744  frecuzrdgfunlem  9747  iseqvalt  9783  iseqoveq  9791  iseqss  9792  iseqsst  9793  iseqfveq2  9795  iseqshft2  9799  monoord  9802  iseqsplit  9805  iseqcaopr3  9807  iseqf1olemp  9828  iseqid3s  9834  iseqid2  9836  iseqhomo  9837  iseqz  9838  expivallem  9847  expcllem  9857  expap0  9876  mulexp  9885  expadd  9888  expmul  9891  leexp2r  9900  leexp1a  9901  bernneq  9963  facdiv  10035  faclbnd  10038  faclbnd6  10041  omgadd  10099  iseqcoll  10136  shftvalg  10159  shftval4g  10160  cjexp  10215  resqrexlemover  10331  resqrexlemdecn  10333  resqrexlemlo  10334  resqrexlemcalc3  10337  absexp  10400  climshft  10578  climub  10617  climserile  10618  dvdsfac  10728  infssuzex  10812  bezoutlemstep  10853  bezoutlemmain  10854  bezoutlemex  10857  dfgcd2  10870  gcdmultiple  10876  rplpwr  10883  nn0seqcvgd  10890  ialginv  10896  ialgcvga  10900  ialgfx  10901  isprm4  10968  prmind2  10969  prmdvdsexp  10994  prmfac1  10998  bdbm1.3ii  11212  bj-2inf  11263  bj-omtrans  11281  nninfalllemn  11328  nninfalllem1  11329  nninfsellemdc  11332  nninfsellemqall  11337
  Copyright terms: Public domain W3C validator