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

Step	Hyp	Ref	Expression
1		imbid.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	a1d 25	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 ↔ 𝜒)))
3	2	pm5.74d 261	1 ⊢ (𝜑 → ((𝜃 → 𝜓) ↔ (𝜃 → 𝜒)))

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  imbi12d  333  imbi2  337  pm5.42  569  orbi2d  734  con3ALT  1026  con3OLD  1029  axc15  2291  ax12v2OLD  2330  axc14  2360  mo2  2467  2gencl  3209  3gencl  3210  vtocl2gf  3241  vtocl3gf  3242  vtocl4g  3250  eqeu  3344  mo2icl  3352  euind  3360  reu7  3368  reuind  3378  sbctt  3467  sbcnestgf  3947  r19.36zv  4024  dedth2h  4090  dedth3h  4091  dedth4h  4092  preq12bg  4326  prel12g  4327  elint  4416  elintrabg  4424  intab  4442  trssOLD  4690  axrep1  4700  axrep2  4701  axrep3  4702  bm1.3ii  4712  reusv3  4802  pocl  4966  swopolem  4968  solin  4982  freq1  5008  frminex  5018  vtoclr  5086  2optocl  5119  3optocl  5120  raliunxp  5183  resieq  5327  iss  5367  cnveqb  5508  preddowncl  5624  funmo  5820  funimaexg  5889  fnbrfvb  6146  fvelimab  6163  fvmptss  6201  fmptco  6303  fprg  6327  fnressn  6330  fressnfv  6332  isoselem  6491  ovg  6697  caovcan  6736  caovordig  6737  caovord  6743  tfisi  6950  tfindsg  6952  tfinds2  6955  tfinds3  6956  dfom2  6959  elom  6960  findsg  6985  finds2  6986  f1o2ndf1  7172  poxp  7176  fnse  7181  wfr3g  7300  wfrlem4  7305  smoeq  7334  smores  7336  smogt  7351  tfrlem1  7359  tfr3  7382  oaordi  7513  oeordi  7554  oeoa  7564  oeoe  7566  nnacl  7578  nnmcl  7579  nnecl  7580  nnacom  7584  nnaordi  7585  nnawordi  7588  nnaass  7589  nndi  7590  nnmass  7591  nnmsucr  7592  nnmcom  7593  nnmordi  7598  2ecoptocl  7725  3ecoptocl  7726  undifixp  7830  xpdom2g  7941  findcard2  8085  xpfi  8116  fnfi  8123  fodomfi  8124  finsschain  8156  marypha1lem  8222  marypha1  8223  supeq1  8234  ordiso2  8303  ordtypelem7  8312  wemaplem1  8334  inf3lem2  8409  inf3lem5  8412  infdiffi  8438  cantnfval2  8449  cantnfle  8451  cantnfp1lem3  8460  oemapval  8463  cantnflem1  8469  cantnf  8473  wemapwe  8477  cnfcom  8480  cnfcom3clem  8485  tz9.1  8488  r1pwALT  8592  cplem2  8636  karden  8641  infxpenc2lem2  8726  fseqenlem1  8730  dfac8clem  8738  alephinit  8801  dfac4  8828  dfac5lem5  8833  dfac2a  8835  dfac2  8836  dfacacn  8846  dfac12lem3  8850  kmlem2  8856  kmlem13  8867  ackbij1lem16  8940  sornom  8982  infpssrlem4  9011  fin23lem14  9038  fin23lem32  9049  fin23lem34  9051  fin23lem36  9053  isf32lem1  9058  isf32lem2  9059  axcc2lem  9141  axcc3  9143  axcclem  9162  zornn0g  9210  ttukeylem5  9218  ttukeylem6  9219  axrepnd  9295  axpowndlem3  9300  zfcndrep  9315  fpwwe2lem8  9338  pwfseqlem3  9361  wunr1om  9420  wunfi  9422  tskr1om  9468  ingru  9516  grudomon  9518  axgroth3  9532  axgroth4  9533  nqereu  9630  mulcanenq  9661  elnp  9688  elnpi  9689  prlem934  9734  infm3  10861  nnaddcl  10919  nnmulcl  10920  peano5uzi  11342  uzind2  11346  nn0indd  11350  zindd  11354  eluzadd  11592  uzaddcl  11620  uzwo  11627  indstr  11632  zmax  11661  xmulasslem  11987  xrsupsslem  12009  xrinfmsslem  12010  xrsupss  12011  xrinfmss  12012  flval2  12477  om2uzlti  12611  uzrdgfni  12619  rabssnn0fi  12647  mptnn0fsupp  12659  seqcl2  12681  seqfveq2  12685  seqshft2  12689  monoord  12693  seqsplit  12696  seqcaopr3  12698  seqf1olem2a  12701  seqf1o  12704  seqid2  12709  seqhomo  12710  ser1const  12719  expcllem  12733  expeq0  12752  mulexp  12761  expadd  12764  expmul  12767  leexp2r  12780  leexp1a  12781  bernneq  12852  modexp  12861  facdiv  12936  faclbnd  12939  faclbnd4lem4  12945  faclbnd6  12948  hashgadd  13027  hashxp  13081  hashmap  13082  hashf1lem2  13097  hashf1  13098  seqcoll  13105  wrdind  13328  wrd2ind  13329  swrdccatin12lem3  13341  cshweqrep  13418  2cshwcshw  13422  relexp0g  13610  relexpsucnnr  13613  relexpsucnnl  13620  relexpcnv  13623  relexpnndm  13629  relexpaddnn  13639  dfrtrclrec2  13645  rtrclreclem1  13646  rtrclreclem2  13647  rtrclreclem4  13649  dfrtrcl2  13650  relexpind  13652  cjexp  13738  absexp  13892  rlim  14074  rlim2  14075  rlim0  14087  rlim0lt  14088  rlimi  14092  ello12r  14096  ello1mpt  14100  ello1d  14102  elo12r  14107  lo1o1  14111  o1lo1  14116  lo1res  14138  climshft  14155  o1compt  14166  rlimo1  14195  lo1add  14205  lo1mul  14206  rlimdiv  14224  climub  14240  climserle  14241  caucvgrlem  14251  caurcvgr  14252  iseraltlem2  14261  summolem2a  14293  sumss  14302  fsum2d  14344  fsumabs  14374  fsumrlim  14384  fsumo1  14385  fsumiun  14394  binom  14401  bcxmas  14406  climcndslem1  14420  climcndslem2  14421  cvgrat  14454  clim2prod  14459  prodfn0  14465  prodfrec  14466  ntrivcvgfvn0  14470  prodmolem2a  14503  fprodabs  14543  fprodn0  14548  fprod2d  14550  binomfallfac  14611  bpolycl  14622  bpolydif  14625  fprodefsum  14664  demoivreALT  14770  ruclem8  14805  ruclem9  14806  dvdsle  14870  dvdsfac  14886  divalglem7  14960  bitsinv1  15002  sadcadd  15018  sadadd2  15020  saddisjlem  15024  smuval2  15042  smupvallem  15043  smu01lem  15045  smupval  15048  smueqlem  15050  smumullem  15052  bezoutlem4  15097  dfgcd2  15101  gcdmultiple  15107  rplpwr  15114  nn0seqcvgd  15121  seq1st  15122  alginv  15126  algcvga  15130  algfx  15131  lcmf  15184  prmind2  15236  prmdvdsexp  15265  prmfac1  15269  reumodprminv  15347  pcmpt  15434  pcfac  15441  prmpwdvds  15446  prmreclem4  15461  vdwlem10  15532  ramval  15550  ramcl  15571  cshwrepswhash1  15647  prmlem1a  15651  imasleval  16024  ismre  16073  mreexexd  16131  mreexexdOLD  16132  lubprop  16809  lublecllem  16811  glbprop  16822  joinlem  16834  meetlem  16848  isglbd  16940  lubun  16946  poslubmo  16969  posglbmo  16970  poslubd  16971  mrcmndind  17189  frmdgsum  17222  mulgnnass  17399  mulgnnassOLD  17400  mhmmulg  17406  gsumwrev  17619  gsmsymgrfix  17671  gsmsymgreq  17675  psgnunilem3  17739  sylow1lem1  17836  efginvrel2  17963  efgsrel  17970  efgredlemd  17980  efgredlem  17983  efgred  17984  efgrelexlemb  17986  gsum2dlem2  18193  gsumcom2  18197  ablfac1eulem  18294  pgpfac1lem2  18297  pgpfac1lem5  18301  pgpfac1  18302  pgpfac  18306  srgmulgass  18354  srgpcomp  18355  srgbinom  18368  lmodvsmmulgdi  18721  isdomn2  19120  assamulgscm  19171  mplcoe1  19286  mplcoe3  19287  mplcoe5  19289  gsummoncoe1  19495  cnfldexp  19598  islindf4  19996  dmatval  20117  dmatel  20118  dmatmulcl  20125  pmatcoe1fsupp  20325  decpmataa0  20392  decpmatmulsumfsupp  20397  pmatcollpw2lem  20401  pm2mpmhmlem1  20442  fiinopn  20531  mretopd  20706  neiptoptop  20745  cnpfval  20848  iscnp3  20858  tgcn  20866  lmbr  20872  lmbr2  20873  lmbrf  20874  lmss  20912  ishaus  20936  hausnei2  20967  t1sep2  20983  fiuncmp  21017  dfcon2  21032  1stcfb  21058  2ndc1stc  21064  1stcrest  21066  1stcelcls  21074  1stccn  21076  lly1stc  21109  elkgen  21149  kgencn  21169  tx1stc  21263  xkopt  21268  cnmptcom  21291  isr0  21350  r0sep  21361  ptcmpfi  21426  isfildlem  21471  rnelfm  21567  fbflim  21590  flimrest  21597  isflf  21607  flffbas  21609  lmflf  21619  fclsrest  21638  isfcf  21648  cnextfvval  21679  tmdmulg  21706  tmdgsum  21709  eltsms  21746  tsmsi  21747  tsmsgsum  21752  tsmssubm  21756  tsmsres  21757  tsmsf1o  21758  isust  21817  isucn  21892  isucn2  21893  ucnima  21895  imasdsf1olem  21988  metss  22123  met1stc  22136  metcnp  22156  metcnpi  22159  metcnpi2  22160  metucn  22186  xrge0tsms  22445  fsumcn  22481  elcncf  22500  cncfi  22505  rescncf  22508  cncfco  22518  caucfil  22889  equivcau  22906  caubl  22914  caublcls  22915  ovolgelb  23055  ovolunlem1a  23071  ovolicc2lem3  23094  voliunlem1  23125  voliunlem3  23127  volsuplem  23130  volsup  23131  dyadmax  23172  vitali  23188  itg2leub  23307  itgfsum  23399  dvnadd  23498  dvnres  23500  cpnord  23504  dvnfre  23521  dvmptfsum  23542  dvferm1  23552  dvferm2  23554  rolle  23557  dvlip  23560  c1lip1  23564  lhop1  23581  deg1leb  23659  ply1divex  23700  fta1g  23731  plyco  23801  dgrcolem1  23833  dgrco  23835  dvnply2  23846  plydivex  23856  aalioulem2  23892  aalioulem3  23893  aalioulem5  23895  aaliou3lem2  23902  dvntaylp  23929  taylthlem1  23931  ulmdvlem3  23960  abelthlem9  23998  cxpmul2  24235  scvxcvx  24512  jensenlem2  24514  jensen  24515  wilthlem3  24596  perfectlem2  24755  bcmono  24802  bposlem5  24813  lgsquad2lem2  24910  dchrisumlem1  24978  dchrisum0flb  24999  pntpbnd1  25075  pntlemf  25094  qabvle  25114  qabvexp  25115  ostthlem2  25117  ostth2lem2  25123  tgcgr4  25226  sizeusglecusglem1  26012  2pthoncl  26133  fargshiftf1  26165  3v3e3cycl1  26172  4cycl4v4e  26194  4cycl4dv4e  26196  wlkiswwlk2lem4  26222  wlkiswwlk2  26225  clwlkisclwwlklem2a  26313  clwlkisclwwlklem2  26314  clwlkfoclwwlk  26372  el2wlkonot  26396  el2spthonot  26397  rusgranumwlk  26484  eupatrl  26495  eupath2  26507  frgra3vlem1  26527  3vfriswmgralem  26531  usg2spot2nb  26592  2spotmdisj  26595  numclwlk2lem2f1o  26632  isplig  26720  isnvlem  26849  nvi  26853  nmoubi  27011  nmounbi  27015  nmblolbi  27039  ipasslem1  27070  ipassi  27080  hlim2  27433  pjhth  27636  spansni  27800  elspansn2  27810  pjige0  27934  pjcjt2  27935  pjopyth  27963  elcnop  28100  elcnfn  28125  nmopub  28151  cnopc  28156  nmfnleub  28168  elnlfn  28171  cnfnc  28173  nmbdoplb  28268  nmcexi  28269  nmcoplb  28273  lnfnmul  28291  nmbdfnlb  28293  nmcfnlb  28297  pjss2coi  28407  pjssmi  28408  isst  28456  ishst  28457  stcltr1i  28517  mdbr  28537  dmdbr  28542  mddmd2  28552  mdslmd1lem3  28570  mdslmd1lem4  28571  elat2  28583  atcvat2  28632  cdj1i  28676  vtocl2d  28699  rmoeqALT  28711  iuninc  28761  fmptcof2  28839  nnindd  28953  nn0min  28954  isomnd  29032  omndadd  29037  isarchi2  29070  archirng  29073  archiexdiv  29075  archiabl  29083  xrge0tsmsd  29116  isorng  29130  ofldchr  29145  crefeq  29240  nexple  29399  esumfzf  29458  issiga  29501  isrnsiga  29503  isldsys  29546  ismeas  29589  isrnmeas  29590  measiun  29608  eulerpartlemn  29770  sseqp1  29784  rrvsum  29843  signsply0  29954  signstfvc  29977  bnj941  30097  bnj106  30192  bnj155  30203  bnj590  30234  bnj591  30235  bnj849  30249  bnj893  30252  bnj944  30262  bnj1128  30312  subfacp1lem6  30421  erdszelem8  30434  isscon  30462  cvmliftlem7  30527  cvmliftlem10  30530  cvmlift3lem2  30556  mrsubvrs  30673  mclsssvlem  30713  mclsval  30714  mclsax  30720  mclsind  30721  shftvalg  30870  bccolsum  30878  iprodefisumlem  30879  faclimlem1  30882  dfpo2  30898  br1steqg  30919  br2ndeqg  30920  rdgprc  30944  trpredmintr  30975  frmin  30983  soseq  30995  frr3g  31023  fveleq  31620  unblimceq0  31668  bj-axrep1  31976  bj-axrep2  31977  bj-axrep3  31978  rdgeqoa  32394  finxpreclem6  32409  wl-sblimt  32511  wl-sbhbt  32514  wl-2sb6d  32520  wl-mo2df  32531  wl-mo2t  32536  poimirlem2  32581  poimirlem25  32604  poimirlem28  32607  poimirlem31  32610  heicant  32614  mbfresfi  32626  itg2gt0cn  32635  sdclem2  32708  fdc  32711  seqpo  32713  incsequz  32714  mettrifi  32723  prdsbnd2  32764  heiborlem4  32783  bfplem1  32791  iscringd  32967  maxidlval  33008  igenval2  33035  ax12eq  33244  ax12el  33245  ax12indalem  33248  ax12inda2ALT  33249  ax12inda  33251  ax12v2-o  33252  riotasvd  33260  isopos  33485  isat3  33612  ishlat1  33657  glbconN  33681  ispsubsp  34049  isldil  34414  isltrn  34423  isdilN  34459  trlval  34467  cdleme27b  34674  cdleme29b  34681  cdleme31sn1  34687  cdleme31sn1c  34694  cdleme40v  34775  cdlemk36  35219  cdlemkid5  35241  cdlemn11pre  35517  dihord2pre  35532  islpolN  35790  hdmapffval  36136  hdmapfval  36137  hdmapval2lem  36141  ismrc  36282  incssnn0  36292  mzpexpmpt  36326  pell14qrexpclnn0  36448  monotuz  36524  expmordi  36530  rmxypos  36532  jm2.17a  36545  jm2.17b  36546  rmygeid  36549  jm2.18  36573  jm2.19lem3  36576  jm2.25  36584  jm2.15nn0  36588  jm2.16nn0  36589  wepwsolem  36630  aomclem8  36649  dfac11  36650  pwslnm  36682  lnr2i  36705  hbtlem5  36717  cnsrexpcl  36754  rngunsnply  36762  isdomn3  36801  ifpbi23  36836  elmapintrab  36901  elmapintab  36921  cnvcnvintabd  36925  eliunov2  36990  relexpxpnnidm  37014  relexpiidm  37015  relexpss1d  37016  iunrelexpmin1  37019  relexpmulnn  37020  iunrelexpmin2  37023  relexp0a  37027  trclimalb2  37037  clsk3nimkb  37358  ntrclsiso  37385  ntrclskb  37387  ntrneiiso  37409  ntrneix2  37411  ntrneixb  37413  gneispace2  37450  gneispacess2  37464  dvgrat  37533  pm14.122b  37646  fnchoice  38211  fiiuncl  38259  ssinc  38292  ssdec  38293  wessf1ornlem  38366  dmrelrnrel  38414  fperiodmullem  38458  fmul01  38647  fmuldfeq  38650  climsuselem1  38674  climinff  38678  ellimcabssub0  38684  limcleqr  38711  addlimc  38715  0ellimcdiv  38716  limclner  38718  dvnmptdivc  38828  dvnmptconst  38831  dvnmul  38833  iblspltprt  38865  itgspltprt  38871  stoweidlem2  38895  stoweidlem3  38896  stoweidlem17  38910  stoweidlem19  38912  stoweidlem21  38914  stoweidlem26  38919  fourierdlem42  39042  issal  39210  ismea  39344  isome  39384  carageniuncllem1  39411  caratheodorylem1  39416  smonoord  39944  perfectALTVlem2  40165  2ffzoeq  40361  usgr2pth  40970  1wlkiswwlks2lem4  41069  1wlkiswwlks2  41072  rusgrnumwwlk  41178  clwlkclwwlklem2a  41207  clwlkclwwlklem1  41208  clwlksfoclwwlk  41270  eupth2  41407  frgr3vlem1  41443  3vfriswmgrlem  41447  3vfriswmgr  41448  av-numclwlk2lem2f1o  41535  lmodvsmdi  41957  dmatALTval  41983  dmatALTbasel  41985  snlindsntor  42054  ldepsnlinc  42091  elbigo2r  42145  elbigolo1  42149  setrecseq  42231  setrec2fun  42238  setrec2lem2  42240