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

Theorem anbi12i 728
Description: Conjoin both sides of two equivalences. (Contributed by NM, 12-Mar-1993.)
Hypotheses
Ref Expression
anbi12.1 (𝜑𝜓)
anbi12.2 (𝜒𝜃)
Assertion
Ref Expression
anbi12i ((𝜑𝜒) ↔ (𝜓𝜃))

Proof of Theorem anbi12i
StepHypRef Expression
1 anbi12.1 . . 3 (𝜑𝜓)
21anbi1i 726 . 2 ((𝜑𝜒) ↔ (𝜓𝜒))
3 anbi12.2 . . 3 (𝜒𝜃)
43anbi2i 725 . 2 ((𝜓𝜒) ↔ (𝜓𝜃))
52, 4bitri 262 1 ((𝜑𝜒) ↔ (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wb 194  wa 382
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 195  df-an 384
This theorem is referenced by:  anbi12ci  729  ordi  903  ordir  904  orddi  908  pm5.17  927  xor  930  3anbi123i  1243  an6  1399  nanbi  1445  cadan  1538  nic-axALT  1589  19.43OLD  1799  sbequ8  1871  sbbi  2388  sbnf2  2426  2mo2  2537  2eu4  2543  sbabel  2778  neanior  2873  rexeqbii  3035  r19.26m  3048  reean  3084  2ralor  3087  reu5  3135  reu2  3360  reu3  3362  2reu5lem3  3381  eqss  3582  unss  3748  ralunb  3755  ssin  3796  undi  3832  indifdir  3841  undif3  3846  undif3OLD  3847  inab  3853  difab  3854  reuss2  3865  reupick  3869  prssOLD  4291  sstp  4302  tpss  4303  prneimg  4323  prnebg  4324  uniin  4387  intun  4438  intpr  4439  disjiun  4567  disjxiun  4573  disjxiunOLD  4574  brin  4628  brdif  4629  ssext  4843  pweqb  4845  opthg2  4867  copsex4g  4878  eqopab2b  4919  pwin  4931  pofun  4964  wetrep  5020  elxp3  5081  soinxp  5095  weinxp  5098  csbxp  5112  relun  5146  inopab  5161  difopab  5162  inxp  5163  opelco2g  5198  cnvco  5217  dmin  5240  restidsing  5363  intasym  5416  asymref  5417  asymref2  5418  cnvdif  5443  xpnz  5457  difxp  5462  xpdifid  5466  xp11  5473  dfco2  5536  relssdmrn  5558  cnvpo  5575  cnvso  5576  xpco  5577  dffun4  5801  funun  5831  fun11  5862  fununi  5863  imadif  5872  fnres  5906  mptfnf  5913  fnopabg  5915  fun  5964  fin  5982  dff1o2  6039  brprcneu  6080  dffv2  6165  fsn  6292  f13dfv  6407  dff1o6  6408  isotr  6463  eqoprab2b  6588  porpss  6816  sucelon  6886  elxp6  7068  dfoprab3  7092  opiota  7095  fsplit  7146  poxp  7153  soxp  7154  suppvalbr  7163  brtpos2  7222  wfrlem5  7283  wfrfun  7289  tfrlem7  7343  dfer2  7607  eqer  7641  eqerOLD  7642  iiner  7683  uniinqs  7691  brecop  7704  eroveu  7706  erovlem  7707  mapval2  7750  ixpin  7796  boxriin  7813  brsdom  7841  xpcomco  7912  xpassen  7916  sbthlem9  7940  sbthlem10  7941  brsdom2  7946  ssenen  7996  unfi  8089  dffi3  8197  dfsup2  8210  infcllem  8253  axinf2  8397  zfinf2  8399  oemapso  8439  scottexs  8610  scott0s  8611  kardex  8617  karden  8618  dfac5lem1  8806  dfac5lem3  8808  kmlem15  8846  enfin2i  9003  fin23lem34  9028  brdom7disj  9211  fpwwe2lem12  9319  fpwwe2lem13  9320  axgroth5  9502  grothprim  9512  addsrpr  9752  mulsrpr  9753  mulgt0sr  9782  addcnsr  9812  mulcnsr  9813  ltresr  9817  axcnre  9841  1re  9895  ssxr  9958  infrenegsup  10855  nnwos  11589  zmin  11618  xrnemnf  11790  xrnepnf  11791  xmullem  11925  xmulcom  11927  xmulneg1  11930  xmulf  11933  xrinfmss2  11971  elfzuzb  12164  fzass4  12207  seqof  12677  hashbclem  13047  hashfacen  13049  xpcogend  13509  trclublem  13530  rexanre  13882  caubnd  13894  o1lo1  14064  rpnnen2lem12  14741  lcmcllem  15095  lcmftp  15135  lcmfunsnlem2  15139  isprm3  15182  prmreclem2  15407  4sqlem12  15446  isffth2  16347  fucinv  16404  lublecllem  16759  oduglb  16910  odulub  16912  issubm  17118  issubmd  17120  isnsg2  17395  oppgid  17557  symgfixf1  17628  pmtrrn2  17651  lsmdisjr  17868  lsmhash  17889  dprd0  18201  issrg  18278  dvdsrtr  18423  isirred2  18472  lss1d  18732  lspsolvlem  18911  lbsextlem2  18928  evlsval  19288  unocv  19790  iunocv  19791  gsumcom3  19971  mpt2matmul  20018  cpmidpmat  20444  tgval2  20518  fctop  20565  ppttop  20568  epttop  20570  cnnei  20843  2ndcctbss  21015  txuni2  21125  txbas  21127  ptbasin  21137  txdis1cn  21195  xkococnlem  21219  opnfbas  21403  fgcl  21439  fbasrn  21445  filuni  21446  cfinfil  21454  csdfil  21455  fin1aufil  21493  rnelfmlem  21513  fmfnfmlem3  21517  txflf  21567  xmeterval  21994  reconn  22386  iimulcl  22491  isclmp  22652  iscau3  22828  rrxmvallem  22939  minveclem3  22952  pmltpc  22970  ovolfcl  22986  ismbl  23045  dyaddisj  23114  iblre  23310  plyun0  23701  logfaclbnd  24691  lgslem3  24768  lgsdir2lem5  24798  ishpg  25396  nb3grapr2  25776  cusgra3v  25786  4cycl4v4e  25987  4cycl4dv4e  25989  wlknwwlkninj  26032  wlkiswwlkinj  26039  wwlknndef  26058  clwwlknndef  26094  clwwlkf1  26117  frisusgranb  26317  frgra3v  26322  ajfval  26841  issh  27242  chcon2i  27500  chcon3i  27502  spanuni  27580  5oalem7  27696  3oalem3  27700  pjin2i  28229  pjin3i  28230  cvnbtwn4  28325  mdslj1i  28355  mdslj2i  28356  mdslmd1i  28365  chrelat4i  28409  chirredi  28430  cdj3i  28477  iuninc  28554  fcoinvbr  28592  suppss2f  28612  fmptdF  28629  disjdsct  28656  cnvoprab  28679  f1od2  28680  tosglblem  28793  pmtrprfv2  28972  ordtconlem1  29091  esumpfinvalf  29258  esum2dlem  29274  measiuns  29400  eulerpartlemt0  29551  eulerpartlemr  29556  eulerpartlemn  29563  ballotlem2  29670  ballotlemodife  29679  bnj887  29882  bnj976  29895  bnj1385  29950  bnj153  29997  bnj543  30010  bnj607  30033  bnj882  30043  bnj916  30050  bnj983  30068  derangenlem  30200  pconcon  30260  elmpst  30480  dftr6  30686  dffr5  30689  dfpo2  30691  fundmpss  30703  elpotr  30723  soseq  30788  frrlem5  30821  frrlem5c  30823  nocvxmin  30883  brtxp  30950  brpprod  30955  brsset  30959  idsset  30960  dfon3  30962  ellimits  30980  dffun10  30984  elfuns  30985  brcart  31002  brimg  31007  brapply  31008  brcap  31010  brsuccf  31011  funpartfun  31013  dfrecs2  31020  dfrdg4  31021  altopthc  31041  altopthd  31042  altopelaltxp  31046  outsideoftr  31199  trer  31273  gtinfOLD  31277  neibastop1  31317  neifg  31329  df3nandALT1  31359  imnand2  31362  bj-eldiag2  32052  topdifinfeq  32157  relowlssretop  32170  relowlpssretop  32171  wl-cases2-dnf  32257  poimirlem30  32392  poimirlem32  32394  ismblfin  32403  mbfposadd  32410  inixp  32476  elghomOLD  32639  keridl  32784  smprngopr  32804  sbcani  32863  prtlem10  32951  prter1  32965  lcvbr3  33111  isopos  33268  llnexatN  33608  snatpsubN  33837  pclclN  33978  pclfinN  33987  lhpocnel2  34106  cdlemk19w  35061  dih1dimatlem  35419  mzpclall  36091  mzpincl  36098  mzpindd  36110  2nn0ind  36311  dford4  36397  wopprc  36398  islmodfg  36440  isdomn3  36584  ifpan123g  36605  ifpan23  36606  ifpdfbi  36620  ifpnot23  36625  ifpdfxor  36634  ifpidg  36638  ifpid1g  36641  ifpim23g  36642  ifpim123g  36647  ifpim1g  36648  ifp1bi  36649  ifpimimb  36651  ifpororb  36652  ifpor123g  36655  ifpbibib  36657  rp-isfinite6  36666  undmrnresiss  36712  cotrintab  36723  brtrclfv2  36821  dfxor4  36860  snhesn  36883  dffrege76  37036  uneqsn  37124  nzin  37322  onfrALTlem5  37561  onfrALTlem4  37562  undif3VD  37923  onfrALTlem5VD  37926  onfrALTlem4VD  37927  ndisj2  38026  ellimcabssub0  38467  fourierdlem103  38885  fourierdlem104  38886  fourierdlem112  38894  smflim  39446  2reu5a  39609  2reu1  39618  2reu4a  39621  propeqop  40105  usgrexmpllem  40465  nb3grpr2  40592  vtxd0nedgb  40684  1wlk1walk  40824  wspthnonp  41036  wwlksn0s  41038  wlknwwlksninj  41067  wlkwwlkinj  41074  wwlksnndef  41092  wwlksnfi  41093  21wlkdlem8  41121  elwwlks2s3  41150  clwwlksnndef  41179  clwwlksf1  41205  3pthdlem1  41312  upgr4cycl4dv4e  41333  frcond3  41421  av-numclwwlkovf2  41496  av-frgrareg  41529  issubmgm  41560  rabsubmgmd  41562  2zlidl  41705  mndpsuppss  41927  islininds2  42048  zlmodzxzldeplem3  42066  alsi-no-surprise  42293
  Copyright terms: Public domain W3C validator