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

Theorem anbi12i 612
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 610 . 2 ((𝜑𝜒) ↔ (𝜓𝜒))
3 anbi12.2 . . 3 (𝜒𝜃)
43anbi2i 609 . 2 ((𝜓𝜒) ↔ (𝜓𝜃))
52, 4bitri 264 1 ((𝜑𝜒) ↔ (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wb 196  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 197  df-an 383
This theorem is referenced by:  anbi12ci  613  ordi  985  ordir  986  orddi  989  pm5.17  992  xor  995  cases2  1032  3anbi123i  1158  an6  1556  nanbi  1602  cadan  1696  nic-axALT  1747  19.43OLD  1963  sbequ8  2054  sbbi  2548  sbnf2  2589  2mo2  2699  2eu4  2705  sbabel  2942  neanior  3035  rexeqbii  3202  r19.26m  3215  reean  3254  2ralor  3257  reu5  3308  reu2  3546  reu3  3548  2reu5lem3  3567  eqss  3767  unss  3938  ralunb  3945  ssin  3983  undi  4023  indifdir  4032  undif3  4037  inab  4043  difab  4044  reuss2  4055  reupick  4059  ssdifsnOLD  4455  sstp  4500  tpss  4501  prneimg  4519  prnebg  4520  uniin  4594  intun  4643  intpr  4644  disjiun  4774  disjxiun  4783  brin  4838  brdif  4839  ssext  5051  pweqb  5053  opthg2  5075  copsex4g  5086  propeqop  5100  eqopab2b  5138  pwin  5151  pofun  5186  wetrep  5242  elxp3  5309  soinxp  5323  weinxp  5326  csbxp  5340  relun  5374  inopab  5391  difopab  5392  inxp  5393  opelco2g  5428  cnvco  5446  dmin  5470  restidsing  5599  intasym  5652  asymref  5653  asymref2  5654  cnvdif  5680  xpnz  5694  difxp  5699  xpdifid  5703  xp11  5710  dfco2  5778  relssdmrn  5800  cnvpo  5817  cnvso  5818  xpco  5819  dffun4  6043  funun  6075  fun11  6103  fununi  6104  imadif  6113  fnres  6147  mptfnf  6155  fnopabg  6157  fun  6206  fin  6225  dff1o2  6283  brprcneu  6325  dffv2  6413  fsn  6545  f13dfv  6673  dff1o6  6674  isotr  6729  eqoprab2b  6860  porpss  7088  sucelon  7164  elxp6  7349  dfoprab3  7373  opiota  7378  fsplit  7433  poxp  7440  soxp  7441  suppvalbr  7450  brtpos2  7510  wfrlem5  7572  wfrfun  7578  tfrlem7  7632  dfer2  7897  eqer  7931  iiner  7971  uniinqs  7979  brecop  7992  eroveu  7995  erovlem  7996  mapval2  8039  ixpin  8087  boxriin  8104  brsdom  8132  xpcomco  8206  xpassen  8210  sbthlem9  8234  sbthlem10  8235  brsdom2  8240  ssenen  8290  unfi  8383  dffi3  8493  dfsup2  8506  infcllem  8549  axinf2  8701  zfinf2  8703  oemapso  8743  scottexs  8914  scott0s  8915  kardex  8921  karden  8922  dfac5lem1  9146  dfac5lem3  9148  kmlem15  9188  enfin2i  9345  fin23lem34  9370  brdom7disj  9555  fpwwe2lem12  9665  fpwwe2lem13  9666  axgroth5  9848  grothprim  9858  addsrpr  10098  mulsrpr  10099  mulgt0sr  10128  addcnsr  10158  mulcnsr  10159  ltresr  10163  axcnre  10187  1re  10241  ssxr  10309  infrenegsup  11208  nnwos  11958  zmin  11987  xrnemnf  12156  xrnepnf  12157  xmullem  12299  xmulcom  12301  xmulneg1  12304  xmulf  12307  xrinfmss2  12346  elfzuzb  12543  fzass4  12586  seqof  13065  hashbclem  13438  hashfacen  13440  xpcogend  13923  trclublem  13944  rexanre  14294  caubnd  14306  o1lo1  14476  rpnnen2lem12  15160  lcmcllem  15517  lcmftp  15557  lcmfunsnlem2  15561  isprm3  15603  prmreclem2  15828  4sqlem12  15867  isffth2  16783  fucinv  16840  lublecllem  17196  oduglb  17347  odulub  17349  issubm  17555  issubmd  17557  isnsg2  17832  oppgid  17993  symgfixf1  18064  pmtrrn2  18087  lsmdisjr  18304  lsmhash  18325  dprd0  18638  issrg  18715  dvdsrtr  18860  isirred2  18909  lss1d  19176  lspsolvlem  19356  lbsextlem2  19374  evlsval  19734  cnfldfunALT  19974  unocv  20241  iunocv  20242  gsumcom3  20422  mpt2matmul  20470  cpmidpmat  20898  tgval2  20981  fctop  21029  ppttop  21032  epttop  21034  cnnei  21307  2ndcctbss  21479  txuni2  21589  txbas  21591  ptbasin  21601  txdis1cn  21659  xkococnlem  21683  opnfbas  21866  fgcl  21902  fbasrn  21908  filuni  21909  cfinfil  21917  csdfil  21918  fin1aufil  21956  rnelfmlem  21976  fmfnfmlem3  21980  txflf  22030  xmeterval  22457  reconn  22851  iimulcl  22956  isclmp  23116  iscau3  23295  rrxmvallem  23406  minveclem3  23419  pmltpc  23438  ovolfcl  23454  ismbl  23514  dyaddisj  23584  iblre  23780  plyun0  24173  logfaclbnd  25168  lgslem3  25245  lgsdir2lem5  25275  ishpg  25872  usgrexmpllem  26375  nb3grpr2  26508  vtxd0nedgb  26619  wlk1walk  26770  clwlkcompbp  26913  wwlknllvtx  26975  wwlksonvtx  26985  wspthnonp  26993  wwlksn0s  26995  wlknwwlksninjOLD  27023  wlkwwlkinjOLD  27031  wwlksnndef  27049  wwlksnfi  27050  2wlkdlem8  27080  elwwlks2s3  27098  clwwlkf1  27205  clwwlknonccat  27271  clwwlknon2x  27278  3pthdlem1  27344  upgr4cycl4dv4e  27365  frgr2wwlk1  27511  frgrreg  27593  ajfval  28004  issh  28405  chcon2i  28663  chcon3i  28665  spanuni  28743  5oalem7  28859  3oalem3  28863  pjin2i  29392  pjin3i  29393  cvnbtwn4  29488  mdslj1i  29518  mdslj2i  29519  mdslmd1i  29528  chrelat4i  29572  chirredi  29593  cdj3i  29640  difrab2  29677  iuninc  29717  fcoinvbr  29757  suppss2f  29779  fmptdF  29796  disjdsct  29820  cnvoprabOLD  29838  f1od2  29839  tosglblem  30009  pmtrprfv2  30188  ordtconnlem1  30310  esumpfinvalf  30478  esum2dlem  30494  measiuns  30620  eulerpartlemt0  30771  eulerpartlemr  30776  eulerpartlemn  30783  ballotlem2  30890  ballotlemodife  30899  bnj887  31173  bnj976  31186  bnj1385  31241  bnj153  31288  bnj543  31301  bnj607  31324  bnj882  31334  bnj916  31341  bnj983  31359  derangenlem  31491  pconnconn  31551  elmpst  31771  dftr6  31978  dffr5  31981  dfpo2  31983  fundmpss  32002  elpotr  32022  soseq  32091  frrlem5  32121  frrlem5c  32123  nocvxmin  32231  sltrec  32261  brtxp  32324  brpprod  32329  brsset  32333  idsset  32334  dfon3  32336  ellimits  32354  dffun10  32358  elfuns  32359  brcart  32376  brimg  32381  brapply  32382  brcap  32384  brsuccf  32385  funpartfun  32387  dfrecs2  32394  dfrdg4  32395  altopthc  32415  altopthd  32416  altopelaltxp  32420  outsideoftr  32573  trer  32647  gtinfOLD  32651  neibastop1  32691  neifg  32703  df3nandALT1  32733  imnand2  32736  bj-eldiag2  33429  topdifinfeq  33535  relowlssretop  33548  relowlpssretop  33549  wl-cases2-dnf  33632  poimirlem30  33772  poimirlem32  33774  ismblfin  33783  mbfposadd  33789  inixp  33855  elghomOLD  34018  keridl  34163  smprngopr  34183  sbcani  34242  an2anr  34343  inxpxrn  34495  dfcoss2  34513  1cossres  34526  dfcoels  34527  br1cossinres  34539  br1cossinidres  34541  br1cossincnvepres  34542  br1cossxrnidres  34543  br1cossxrncnvepres  34544  cosscnvssid3  34568  coss0  34571  cossid  34572  trcoss  34574  eleccossin  34575  dfssr2  34591  br1cossxrncnvssrres  34600  refsymrels3  34654  refsymrel2  34655  refsymrel3  34656  elrefsymrels3  34658  prtlem10  34673  prter1  34687  lcvbr3  34832  isopos  34989  llnexatN  35329  snatpsubN  35558  pclclN  35699  pclfinN  35708  lhpocnel2  35827  cdlemk19w  36781  dih1dimatlem  37139  psspwb  37776  mzpclall  37816  mzpincl  37823  mzpindd  37835  2nn0ind  38036  dford4  38122  wopprc  38123  islmodfg  38165  isdomn3  38308  ifpan123g  38329  ifpan23  38330  ifpdfbi  38344  ifpnot23  38349  ifpdfxor  38358  ifpidg  38362  ifpid1g  38365  ifpim23g  38366  ifpim123g  38371  ifpim1g  38372  ifp1bi  38373  ifpimimb  38375  ifpororb  38376  ifpor123g  38379  ifpbibib  38381  rp-isfinite6  38390  undmrnresiss  38436  cotrintab  38447  brtrclfv2  38545  dfxor4  38584  snhesn  38606  dffrege76  38759  uneqsn  38847  nzin  39043  onfrALTlem5  39282  onfrALTlem4  39283  undif3VD  39640  onfrALTlem5VD  39643  onfrALTlem4VD  39644  ndisj2  39739  rexabsle  40162  ellimcabssub0  40367  limsupre2mpt  40480  limsupre3  40483  limsupre3mpt  40484  limsupre3uz  40486  limsupreuz  40487  liminfreuz  40553  fourierdlem103  40943  fourierdlem104  40944  fourierdlem112  40952  smflim  41505  smflim2  41532  smflimsuplem1  41546  smflimsup  41554  2reu5a  41697  2reu1  41706  2reu4a  41709  issubmgm  42317  rabsubmgmd  42319  2zlidl  42462  mndpsuppss  42680  islininds2  42801  zlmodzxzldeplem3  42819  alsi-no-surprise  43073
  Copyright terms: Public domain W3C validator