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

Theorem anbi12i 729
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 727 . 2 ((𝜑𝜒) ↔ (𝜓𝜒))
3 anbi12.2 . . 3 (𝜒𝜃)
43anbi2i 726 . 2 ((𝜓𝜒) ↔ (𝜓𝜃))
52, 4bitri 263 1 ((𝜑𝜒) ↔ (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wb 195  wa 383
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  df-an 385
This theorem is referenced by:  anbi12ci  730  ordi  904  ordir  905  orddi  909  pm5.17  928  xor  931  3anbi123i  1244  an6  1400  nanbi  1446  cadan  1539  nic-axALT  1590  19.43OLD  1800  sbequ8  1872  sbbi  2389  sbnf2  2427  2mo2  2538  2eu4  2544  sbabel  2779  neanior  2874  rexeqbii  3036  r19.26m  3049  reean  3085  2ralor  3088  reu5  3136  reu2  3361  reu3  3363  2reu5lem3  3382  eqss  3583  unss  3749  ralunb  3756  ssin  3797  undi  3833  indifdir  3842  undif3  3847  undif3OLD  3848  inab  3854  difab  3855  reuss2  3866  reupick  3870  prssOLD  4292  sstp  4307  tpss  4308  prneimg  4328  prnebg  4329  uniin  4393  intun  4444  intpr  4445  disjiun  4573  disjxiun  4579  disjxiunOLD  4580  brin  4634  brdif  4635  ssext  4850  pweqb  4852  opthg2  4874  copsex4g  4885  propeqop  4895  eqopab2b  4930  pwin  4942  pofun  4975  wetrep  5031  elxp3  5092  soinxp  5106  weinxp  5109  csbxp  5123  relun  5158  inopab  5174  difopab  5175  inxp  5176  opelco2g  5211  cnvco  5230  dmin  5254  restidsing  5377  intasym  5430  asymref  5431  asymref2  5432  cnvdif  5458  xpnz  5472  difxp  5477  xpdifid  5481  xp11  5488  dfco2  5551  relssdmrn  5573  cnvpo  5590  cnvso  5591  xpco  5592  dffun4  5816  funun  5846  fun11  5877  fununi  5878  imadif  5887  fnres  5921  mptfnf  5928  fnopabg  5930  fun  5979  fin  5998  dff1o2  6055  brprcneu  6096  dffv2  6181  fsn  6308  f13dfv  6430  dff1o6  6431  isotr  6486  eqoprab2b  6611  porpss  6839  sucelon  6909  elxp6  7091  dfoprab3  7115  opiota  7118  fsplit  7169  poxp  7176  soxp  7177  suppvalbr  7186  brtpos2  7245  wfrlem5  7306  wfrfun  7312  tfrlem7  7366  dfer2  7630  eqer  7664  eqerOLD  7665  iiner  7706  uniinqs  7714  brecop  7727  eroveu  7729  erovlem  7730  mapval2  7773  ixpin  7819  boxriin  7836  brsdom  7864  xpcomco  7935  xpassen  7939  sbthlem9  7963  sbthlem10  7964  brsdom2  7969  ssenen  8019  unfi  8112  dffi3  8220  dfsup2  8233  infcllem  8276  axinf2  8420  zfinf2  8422  oemapso  8462  scottexs  8633  scott0s  8634  kardex  8640  karden  8641  dfac5lem1  8829  dfac5lem3  8831  kmlem15  8869  enfin2i  9026  fin23lem34  9051  brdom7disj  9234  fpwwe2lem12  9342  fpwwe2lem13  9343  axgroth5  9525  grothprim  9535  addsrpr  9775  mulsrpr  9776  mulgt0sr  9805  addcnsr  9835  mulcnsr  9836  ltresr  9840  axcnre  9864  1re  9918  ssxr  9986  infrenegsup  10883  nnwos  11631  zmin  11660  xrnemnf  11827  xrnepnf  11828  xmullem  11966  xmulcom  11968  xmulneg1  11971  xmulf  11974  xrinfmss2  12013  elfzuzb  12207  fzass4  12250  seqof  12720  hashbclem  13093  hashfacen  13095  xpcogend  13561  trclublem  13582  rexanre  13934  caubnd  13946  o1lo1  14116  rpnnen2lem12  14793  lcmcllem  15147  lcmftp  15187  lcmfunsnlem2  15191  isprm3  15234  prmreclem2  15459  4sqlem12  15498  isffth2  16399  fucinv  16456  lublecllem  16811  oduglb  16962  odulub  16964  issubm  17170  issubmd  17172  isnsg2  17447  oppgid  17609  symgfixf1  17680  pmtrrn2  17703  lsmdisjr  17920  lsmhash  17941  dprd0  18253  issrg  18330  dvdsrtr  18475  isirred2  18524  lss1d  18784  lspsolvlem  18963  lbsextlem2  18980  evlsval  19340  unocv  19843  iunocv  19844  gsumcom3  20024  mpt2matmul  20071  cpmidpmat  20497  tgval2  20571  fctop  20618  ppttop  20621  epttop  20623  cnnei  20896  2ndcctbss  21068  txuni2  21178  txbas  21180  ptbasin  21190  txdis1cn  21248  xkococnlem  21272  opnfbas  21456  fgcl  21492  fbasrn  21498  filuni  21499  cfinfil  21507  csdfil  21508  fin1aufil  21546  rnelfmlem  21566  fmfnfmlem3  21570  txflf  21620  xmeterval  22047  reconn  22439  iimulcl  22544  isclmp  22705  iscau3  22884  rrxmvallem  22995  minveclem3  23008  pmltpc  23026  ovolfcl  23042  ismbl  23101  dyaddisj  23170  iblre  23366  plyun0  23757  logfaclbnd  24747  lgslem3  24824  lgsdir2lem5  24854  ishpg  25451  nb3grapr2  25983  cusgra3v  25993  4cycl4v4e  26194  4cycl4dv4e  26196  wlknwwlkninj  26239  wlkiswwlkinj  26246  wwlknndef  26265  clwwlknndef  26301  clwwlkf1  26324  frisusgranb  26524  frgra3v  26529  ajfval  27048  issh  27449  chcon2i  27707  chcon3i  27709  spanuni  27787  5oalem7  27903  3oalem3  27907  pjin2i  28436  pjin3i  28437  cvnbtwn4  28532  mdslj1i  28562  mdslj2i  28563  mdslmd1i  28572  chrelat4i  28616  chirredi  28637  cdj3i  28684  iuninc  28761  fcoinvbr  28799  suppss2f  28819  fmptdF  28836  disjdsct  28863  cnvoprab  28886  f1od2  28887  tosglblem  29000  pmtrprfv2  29179  ordtconlem1  29298  esumpfinvalf  29465  esum2dlem  29481  measiuns  29607  eulerpartlemt0  29758  eulerpartlemr  29763  eulerpartlemn  29770  ballotlem2  29877  ballotlemodife  29886  bnj887  30089  bnj976  30102  bnj1385  30157  bnj153  30204  bnj543  30217  bnj607  30240  bnj882  30250  bnj916  30257  bnj983  30275  derangenlem  30407  pconcon  30467  elmpst  30687  dftr6  30893  dffr5  30896  dfpo2  30898  fundmpss  30910  elpotr  30930  soseq  30995  frrlem5  31028  frrlem5c  31030  nocvxmin  31090  brtxp  31157  brpprod  31162  brsset  31166  idsset  31167  dfon3  31169  ellimits  31187  dffun10  31191  elfuns  31192  brcart  31209  brimg  31214  brapply  31215  brcap  31217  brsuccf  31218  funpartfun  31220  dfrecs2  31227  dfrdg4  31228  altopthc  31248  altopthd  31249  altopelaltxp  31253  outsideoftr  31406  trer  31480  gtinfOLD  31484  neibastop1  31524  neifg  31536  df3nandALT1  31566  imnand2  31569  bj-eldiag2  32269  topdifinfeq  32374  relowlssretop  32387  relowlpssretop  32388  wl-cases2-dnf  32474  poimirlem30  32609  poimirlem32  32611  ismblfin  32620  mbfposadd  32627  inixp  32693  elghomOLD  32856  keridl  33001  smprngopr  33021  sbcani  33080  prtlem10  33168  prter1  33182  lcvbr3  33328  isopos  33485  llnexatN  33825  snatpsubN  34054  pclclN  34195  pclfinN  34204  lhpocnel2  34323  cdlemk19w  35278  dih1dimatlem  35636  mzpclall  36308  mzpincl  36315  mzpindd  36327  2nn0ind  36528  dford4  36614  wopprc  36615  islmodfg  36657  isdomn3  36801  ifpan123g  36822  ifpan23  36823  ifpdfbi  36837  ifpnot23  36842  ifpdfxor  36851  ifpidg  36855  ifpid1g  36858  ifpim23g  36859  ifpim123g  36864  ifpim1g  36865  ifp1bi  36866  ifpimimb  36868  ifpororb  36869  ifpor123g  36872  ifpbibib  36874  rp-isfinite6  36883  undmrnresiss  36929  cotrintab  36940  brtrclfv2  37038  dfxor4  37077  snhesn  37100  dffrege76  37253  uneqsn  37341  nzin  37539  onfrALTlem5  37778  onfrALTlem4  37779  undif3VD  38140  onfrALTlem5VD  38143  onfrALTlem4VD  38144  ndisj2  38243  ellimcabssub0  38684  fourierdlem103  39102  fourierdlem104  39103  fourierdlem112  39111  smflim  39663  2reu5a  39826  2reu1  39835  2reu4a  39838  usgrexmpllem  40484  nb3grpr2  40611  vtxd0nedgb  40703  1wlk1walk  40843  wspthnonp  41055  wwlksn0s  41057  wlknwwlksninj  41086  wlkwwlkinj  41093  wwlksnndef  41111  wwlksnfi  41112  21wlkdlem8  41140  elwwlks2s3  41169  clwwlksnndef  41198  clwwlksf1  41224  3pthdlem1  41331  upgr4cycl4dv4e  41352  frcond3  41440  av-numclwwlkovf2  41515  av-frgrareg  41548  issubmgm  41579  rabsubmgmd  41581  2zlidl  41724  mndpsuppss  41946  islininds2  42067  zlmodzxzldeplem3  42085  ssdifsn  42228  alsi-no-surprise  42351
  Copyright terms: Public domain W3C validator