MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imbi2d Structured version   Visualization version   GIF version

Theorem imbi2d 329
Description: Deduction adding an antecedent to both sides of a logical equivalence. (Contributed by NM, 11-May-1993.)
Hypothesis
Ref Expression
imbid.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
imbi2d (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))

Proof of Theorem imbi2d
StepHypRef Expression
1 imbid.1 . . 3 (𝜑 → (𝜓𝜒))
21a1d 25 . 2 (𝜑 → (𝜃 → (𝜓𝜒)))
32pm5.74d 262 1 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197
This theorem is referenced by:  imbi12d  333  imbi2  337  pm5.42  570  orbi2d  738  con3ALT  1052  axc15  2339  axc14  2400  mo2  2507  2gencl  3267  3gencl  3268  vtocl2gf  3299  vtocl3gf  3300  vtocl4g  3308  eqeu  3410  mo2icl  3418  euind  3426  reu7  3434  reuind  3444  sbctt  3533  reu8nf  3549  sbcnestgf  4028  r19.36zv  4105  dedth2h  4173  dedth3h  4174  dedth4h  4175  preq12bg  4417  prel12g  4418  elint  4513  elintrabg  4521  intab  4539  trssOLD  4795  axrep1  4805  axrep2  4806  axrep3  4807  bm1.3ii  4817  reusv3  4906  pocl  5071  swopolem  5073  solin  5087  freq1  5113  frminex  5123  vtoclr  5198  2optocl  5230  3optocl  5231  raliunxp  5294  resieq  5442  iss  5482  cnveqb  5625  preddowncl  5745  funmo  5942  funimaexg  6013  fnbrfvb  6274  fvelimab  6292  fvmptss  6331  fmptco  6436  fprg  6462  fnressn  6465  fressnfv  6467  isoselem  6631  ovg  6841  caovcan  6880  caovordig  6881  caovord  6887  tfisi  7100  tfindsg  7102  tfinds2  7105  tfinds3  7106  dfom2  7109  elom  7110  findsg  7135  finds2  7136  f1o2ndf1  7330  poxp  7334  fnse  7339  wfr3g  7458  wfrlem4  7463  smoeq  7492  smores  7494  smogt  7509  tfrlem1  7517  tfr3  7540  oaordi  7671  oeordi  7712  oeoa  7722  oeoe  7724  nnacl  7736  nnmcl  7737  nnecl  7738  nnacom  7742  nnaordi  7743  nnawordi  7746  nnaass  7747  nndi  7748  nnmass  7749  nnmsucr  7750  nnmcom  7751  nnmordi  7756  2ecoptocl  7881  3ecoptocl  7882  undifixp  7986  xpdom2g  8097  findcard2  8241  xpfi  8272  fnfi  8279  fodomfi  8280  finsschain  8314  marypha1lem  8380  marypha1  8381  supeq1  8392  ordiso2  8461  ordtypelem7  8470  wemaplem1  8492  inf3lem2  8564  inf3lem5  8567  infdiffi  8593  cantnfval2  8604  cantnfle  8606  cantnfp1lem3  8615  oemapval  8618  cantnflem1  8624  cantnf  8628  wemapwe  8632  cnfcom  8635  cnfcom3clem  8640  tz9.1  8643  r1pwALT  8747  cplem2  8791  karden  8796  infxpenc2lem2  8881  fseqenlem1  8885  dfac8clem  8893  alephinit  8956  dfac4  8983  dfac5lem5  8988  dfac2a  8990  dfac2  8991  dfacacn  9001  dfac12lem3  9005  kmlem2  9011  kmlem13  9022  ackbij1lem16  9095  sornom  9137  infpssrlem4  9166  fin23lem14  9193  fin23lem32  9204  fin23lem34  9206  fin23lem36  9208  isf32lem1  9213  isf32lem2  9214  axcc2lem  9296  axcc3  9298  axcclem  9317  zornn0g  9365  ttukeylem5  9373  ttukeylem6  9374  axrepnd  9454  axpowndlem3  9459  zfcndrep  9474  fpwwe2lem8  9497  pwfseqlem3  9520  wunr1om  9579  wunfi  9581  tskr1om  9627  ingru  9675  grudomon  9677  axgroth3  9691  axgroth4  9692  nqereu  9789  mulcanenq  9820  elnp  9847  elnpi  9848  prlem934  9893  infm3  11020  nnaddcl  11080  nnmulcl  11081  peano5uzi  11504  uzind2  11508  nn0indd  11512  zindd  11516  eluzadd  11754  uzaddcl  11782  uzwo  11789  indstr  11794  zmax  11823  xmulasslem  12153  xrsupsslem  12175  xrinfmsslem  12176  xrsupss  12177  xrinfmss  12178  flval2  12655  om2uzlti  12789  uzrdgfni  12797  rabssnn0fi  12825  mptnn0fsupp  12837  seqcl2  12859  seqfveq2  12863  seqshft2  12867  monoord  12871  seqsplit  12874  seqcaopr3  12876  seqf1olem2a  12879  seqf1o  12882  seqid2  12887  seqhomo  12888  ser1const  12897  expcllem  12911  expeq0  12930  mulexp  12939  expadd  12942  expmul  12945  leexp2r  12958  leexp1a  12959  bernneq  13030  modexp  13039  facdiv  13114  faclbnd  13117  faclbnd4lem4  13123  faclbnd6  13126  hashgadd  13204  hashxp  13259  hashmap  13260  hashf1lem2  13278  hashf1  13279  seqcoll  13286  wrdind  13522  wrd2ind  13523  swrdccatin12lem3  13536  cshweqrep  13613  2cshwcshw  13617  relexp0g  13806  relexpsucnnr  13809  relexpsucnnl  13816  relexpcnv  13819  relexpnndm  13825  relexpaddnn  13835  dfrtrclrec2  13841  rtrclreclem1  13842  rtrclreclem2  13843  rtrclreclem4  13845  dfrtrcl2  13846  relexpind  13848  cjexp  13934  absexp  14088  rlim  14270  rlim2  14271  rlim0  14283  rlim0lt  14284  rlimi  14288  ello12r  14292  ello1mpt  14296  ello1d  14298  elo12r  14303  lo1o1  14307  o1lo1  14312  lo1res  14334  climshft  14351  o1compt  14362  rlimo1  14391  lo1add  14401  lo1mul  14402  rlimdiv  14420  climub  14436  climserle  14437  caucvgrlem  14447  caurcvgr  14448  iseraltlem2  14457  summolem2a  14490  sumss  14499  fsum2d  14546  fsumabs  14577  fsumrlim  14587  fsumo1  14588  fsumiun  14597  binom  14606  bcxmas  14611  climcndslem1  14625  climcndslem2  14626  cvgrat  14659  clim2prod  14664  prodfn0  14670  prodfrec  14671  ntrivcvgfvn0  14675  prodmolem2a  14708  fprodabs  14748  fprodn0  14753  fprod2d  14755  binomfallfac  14816  bpolycl  14827  bpolydif  14830  fprodefsum  14869  demoivreALT  14975  ruclem8  15010  ruclem9  15011  dvdsle  15079  dvdsfac  15095  divalglem7  15169  bitsinv1  15211  sadcadd  15227  sadadd2  15229  saddisjlem  15233  smuval2  15251  smupvallem  15252  smu01lem  15254  smupval  15257  smueqlem  15259  smumullem  15261  bezoutlem4  15306  dfgcd2  15310  gcdmultiple  15316  rplpwr  15323  nn0seqcvgd  15330  seq1st  15331  alginv  15335  algcvga  15339  algfx  15340  lcmf  15393  prmind2  15445  prmdvdsexp  15474  prmfac1  15478  reumodprminv  15556  pcmpt  15643  pcfac  15650  prmpwdvds  15655  prmreclem4  15670  vdwlem10  15741  ramval  15759  ramcl  15780  cshwrepswhash1  15856  prmlem1a  15860  imasleval  16248  ismre  16297  mreexexd  16355  mreexexdOLD  16356  lubprop  17033  lublecllem  17035  glbprop  17046  joinlem  17058  meetlem  17072  isglbd  17164  lubun  17170  poslubmo  17193  posglbmo  17194  poslubd  17195  mrcmndind  17413  frmdgsum  17446  mulgnnass  17623  mulgnnassOLD  17624  mhmmulg  17630  gsumwrev  17842  gsmsymgrfix  17894  gsmsymgreq  17898  psgnunilem3  17962  sylow1lem1  18059  efginvrel2  18186  efgsrel  18193  efgredlemd  18203  efgredlem  18206  efgred  18207  efgrelexlemb  18209  gsum2dlem2  18416  gsumcom2  18420  ablfac1eulem  18517  pgpfac1lem2  18520  pgpfac1lem5  18524  pgpfac1  18525  pgpfac  18529  srgmulgass  18577  srgpcomp  18578  srgbinom  18591  lmodvsmmulgdi  18946  isdomn2  19347  assamulgscm  19398  mplcoe1  19513  mplcoe3  19514  mplcoe5  19516  gsummoncoe1  19722  cnfldexp  19827  islindf4  20225  dmatval  20346  dmatel  20347  dmatmulcl  20354  pmatcoe1fsupp  20554  decpmataa0  20621  decpmatmulsumfsupp  20626  pmatcollpw2lem  20630  pm2mpmhmlem1  20671  fiinopn  20754  mretopd  20944  neiptoptop  20983  cnpfval  21086  iscnp3  21096  tgcn  21104  lmbr  21110  lmbr2  21111  lmbrf  21112  lmss  21150  ishaus  21174  hausnei2  21205  t1sep2  21221  fiuncmp  21255  dfconn2  21270  1stcfb  21296  2ndc1stc  21302  1stcrest  21304  1stcelcls  21312  1stccn  21314  lly1stc  21347  elkgen  21387  kgencn  21407  tx1stc  21501  xkopt  21506  cnmptcom  21529  isr0  21588  r0sep  21599  ptcmpfi  21664  isfildlem  21708  rnelfm  21804  fbflim  21827  flimrest  21834  isflf  21844  flffbas  21846  lmflf  21856  fclsrest  21875  isfcf  21885  cnextfvval  21916  tmdmulg  21943  tmdgsum  21946  eltsms  21983  tsmsi  21984  tsmsgsum  21989  tsmssubm  21993  tsmsres  21994  tsmsf1o  21995  isust  22054  isucn  22129  isucn2  22130  ucnima  22132  imasdsf1olem  22225  metss  22360  met1stc  22373  metcnp  22393  metcnpi  22396  metcnpi2  22397  metucn  22423  xrge0tsms  22684  fsumcn  22720  elcncf  22739  cncfi  22744  rescncf  22747  cncfco  22757  caucfil  23127  equivcau  23144  caubl  23152  caublcls  23153  ovolgelb  23294  ovolunlem1a  23310  ovolicc2lem3  23333  voliunlem1  23364  voliunlem3  23366  volsuplem  23369  volsup  23370  dyadmax  23412  vitali  23427  itg2leub  23546  itgfsum  23638  dvnadd  23737  dvnres  23739  cpnord  23743  dvnfre  23760  dvmptfsum  23783  dvferm1  23793  dvferm2  23795  rolle  23798  dvlip  23801  c1lip1  23805  lhop1  23822  deg1leb  23900  ply1divex  23941  fta1g  23972  plyco  24042  dgrcolem1  24074  dgrco  24076  dvnply2  24087  plydivex  24097  aalioulem2  24133  aalioulem3  24134  aalioulem5  24136  aaliou3lem2  24143  dvntaylp  24170  taylthlem1  24172  ulmdvlem3  24201  abelthlem9  24239  cxpmul2  24480  scvxcvx  24757  jensenlem2  24759  jensen  24760  wilthlem3  24841  perfectlem2  25000  bcmono  25047  bposlem5  25058  lgsquad2lem2  25155  dchrisumlem1  25223  dchrisum0flb  25244  pntpbnd1  25320  pntlemf  25339  qabvle  25359  qabvexp  25360  ostthlem2  25362  ostth2lem2  25368  tgcgr4  25471  usgr2pth  26716  wlkiswwlks2lem4  26826  wlkiswwlks2  26829  rusgrnumwwlk  26942  clwlkclwwlklem2a  26964  clwlkclwwlklem1  26965  clwlksfoclwwlk  27050  eupth2  27217  frgr3vlem1  27253  3vfriswmgrlem  27257  3vfriswmgr  27258  numclwlk2lem2f1o  27359  numclwlk2lem2f1oOLD  27366  isplig  27458  isnvlem  27593  nvi  27597  nmoubi  27755  nmounbi  27759  nmblolbi  27783  ipasslem1  27814  ipassi  27824  hlim2  28177  pjhth  28380  spansni  28544  elspansn2  28554  pjige0  28678  pjcjt2  28679  pjopyth  28707  elcnop  28844  elcnfn  28869  nmopub  28895  cnopc  28900  nmfnleub  28912  elnlfn  28915  cnfnc  28917  nmbdoplb  29012  nmcexi  29013  nmcoplb  29017  lnfnmul  29035  nmbdfnlb  29037  nmcfnlb  29041  pjss2coi  29151  pjssmi  29152  isst  29200  ishst  29201  stcltr1i  29261  mdbr  29281  dmdbr  29286  mddmd2  29296  mdslmd1lem3  29314  mdslmd1lem4  29315  elat2  29327  atcvat2  29376  cdj1i  29420  vtocl2d  29442  iuninc  29505  fmptcof2  29585  nnindd  29694  nn0min  29695  isomnd  29829  omndadd  29834  isarchi2  29867  archirng  29870  archiexdiv  29872  archiabl  29880  xrge0tsmsd  29913  isorng  29927  ofldchr  29942  crefeq  30040  nexple  30199  esumfzf  30259  issiga  30302  isrnsiga  30304  isldsys  30347  ismeas  30390  isrnmeas  30391  measiun  30409  eulerpartlemn  30571  sseqp1  30585  rrvsum  30644  signsply0  30756  signstfvc  30779  bnj941  30969  bnj106  31064  bnj155  31075  bnj590  31106  bnj591  31107  bnj849  31121  bnj893  31124  bnj944  31134  bnj1128  31184  subfacp1lem6  31293  erdszelem8  31306  issconn  31334  cvmliftlem7  31399  cvmliftlem10  31402  cvmlift3lem2  31428  mrsubvrs  31545  mclsssvlem  31585  mclsval  31586  mclsax  31592  mclsind  31593  shftvalg  31743  bccolsum  31751  iprodefisumlem  31752  faclimlem1  31755  dfpo2  31771  br1steqgOLD  31798  br2ndeqgOLD  31799  rdgprc  31824  trpredmintr  31855  frmin  31867  soseq  31879  frr3g  31904  nosupno  31974  nosupdm  31975  nosupfv  31977  nosupres  31978  nosupbnd1lem1  31979  nosupbnd1lem3  31981  nosupbnd1lem5  31983  noeta  31993  fveleq  32575  unblimceq0  32623  bj-axrep1  32913  bj-axrep2  32914  bj-axrep3  32915  rdgeqoa  33348  finxpreclem6  33363  wl-sblimt  33462  wl-sbhbt  33465  wl-2sb6d  33471  wl-mo2df  33482  wl-mo2t  33487  poimirlem2  33541  poimirlem25  33564  poimirlem28  33567  poimirlem31  33570  heicant  33574  mbfresfi  33586  itg2gt0cn  33595  sdclem2  33668  fdc  33671  seqpo  33673  incsequz  33674  mettrifi  33683  prdsbnd2  33724  heiborlem4  33743  bfplem1  33751  iscringd  33927  maxidlval  33968  igenval2  33995  iss2  34252  elrefrels3  34408  ax12eq  34545  ax12el  34546  ax12indalem  34549  ax12inda2ALT  34550  ax12inda  34552  ax12v2-o  34553  riotasvd  34560  isopos  34785  isat3  34912  ishlat1  34957  glbconN  34981  ispsubsp  35349  isldil  35714  isltrn  35723  isdilN  35759  trlval  35767  cdleme27b  35973  cdleme29b  35980  cdleme31sn1  35986  cdleme31sn1c  35993  cdleme40v  36074  cdlemk36  36518  cdlemkid5  36540  cdlemn11pre  36816  dihord2pre  36831  islpolN  37089  hdmapffval  37435  hdmapfval  37436  hdmapval2lem  37440  ismrc  37581  incssnn0  37591  mzpexpmpt  37625  pell14qrexpclnn0  37747  monotuz  37823  expmordi  37829  rmxypos  37831  jm2.17a  37844  jm2.17b  37845  rmygeid  37848  jm2.18  37872  jm2.19lem3  37875  jm2.25  37883  jm2.15nn0  37887  jm2.16nn0  37888  wepwsolem  37929  aomclem8  37948  dfac11  37949  pwslnm  37981  lnr2i  38003  hbtlem5  38015  cnsrexpcl  38052  rngunsnply  38060  isdomn3  38099  ifpbi23  38134  elmapintrab  38199  elmapintab  38219  cnvcnvintabd  38223  eliunov2  38288  relexpxpnnidm  38312  relexpiidm  38313  relexpss1d  38314  iunrelexpmin1  38317  relexpmulnn  38318  iunrelexpmin2  38321  relexp0a  38325  trclimalb2  38335  clsk3nimkb  38655  ntrclsiso  38682  ntrclskb  38684  ntrneiiso  38706  ntrneix2  38708  ntrneixb  38710  gneispace2  38747  gneispacess2  38761  dvgrat  38828  pm14.122b  38941  fnchoice  39502  fiiuncl  39548  ssinc  39578  ssdec  39579  wessf1ornlem  39685  dmrelrnrel  39733  fperiodmullem  39831  monoordxrv  40025  fmul01  40130  fmuldfeq  40133  climsuselem1  40157  climinff  40161  ellimcabssub0  40167  limcleqr  40194  addlimc  40198  0ellimcdiv  40199  limclner  40201  limsupref  40235  limsupub  40254  limsupmnf  40271  limsupre2lem  40274  limsupre2  40275  limsupre2mpt  40280  limsupre3lem  40282  limsupre3  40283  limsupre3mpt  40284  xlimbr  40371  cnrefiisplem  40373  dvnmptdivc  40471  dvnmptconst  40474  dvnmul  40476  iblspltprt  40507  itgspltprt  40513  stoweidlem2  40537  stoweidlem3  40538  stoweidlem17  40552  stoweidlem19  40554  stoweidlem21  40556  stoweidlem26  40561  fourierdlem42  40684  issal  40852  ismea  40986  isome  41029  carageniuncllem1  41056  caratheodorylem1  41061  2ffzoeq  41663  smonoord  41666  fargshiftf1  41702  perfectALTVlem2  41956  lmodvsmdi  42488  dmatALTval  42514  dmatALTbasel  42516  snlindsntor  42585  ldepsnlinc  42622  elbigo2r  42672  elbigolo1  42676  setrecseq  42757  setrec2fun  42764  setrec2lem2  42766
  Copyright terms: Public domain W3C validator