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

Theorem anbi12i 733
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 731 . 2 ((𝜑𝜒) ↔ (𝜓𝜒))
3 anbi12.2 . . 3 (𝜒𝜃)
43anbi2i 730 . 2 ((𝜓𝜒) ↔ (𝜓𝜃))
52, 4bitri 264 1 ((𝜑𝜒) ↔ (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384
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 386
This theorem is referenced by:  anbi12ci  734  ordi  908  ordir  909  orddi  913  pm5.17  932  xor  935  3anbi123i  1250  an6  1407  nanbi  1453  cadan  1547  nic-axALT  1598  19.43OLD  1810  sbequ8  1884  sbbi  2400  sbnf2  2438  2mo2  2549  2eu4  2555  sbabel  2792  neanior  2885  rexeqbii  3052  r19.26m  3065  reean  3104  2ralor  3107  reu5  3157  reu2  3392  reu3  3394  2reu5lem3  3413  eqss  3616  unss  3785  ralunb  3792  ssin  3833  undi  3872  indifdir  3881  undif3  3886  undif3OLD  3887  inab  3893  difab  3894  reuss2  3905  reupick  3909  ssdifsn  4316  prssOLD  4350  sstp  4365  tpss  4366  prneimg  4386  prnebg  4387  uniin  4455  intun  4507  intpr  4508  disjiun  4638  disjxiun  4647  disjxiunOLD  4648  brin  4702  brdif  4703  ssext  4921  pweqb  4923  opthg2  4946  copsex4g  4957  propeqop  4968  eqopab2b  5003  pwin  5016  pofun  5049  wetrep  5105  elxp3  5167  soinxp  5181  weinxp  5184  csbxp  5198  relun  5233  inopab  5250  difopab  5251  inxp  5252  opelco2g  5287  cnvco  5306  dmin  5330  restidsing  5456  intasym  5509  asymref  5510  asymref2  5511  cnvdif  5537  xpnz  5551  difxp  5556  xpdifid  5560  xp11  5567  dfco2  5632  relssdmrn  5654  cnvpo  5671  cnvso  5672  xpco  5673  dffun4  5898  funun  5930  fun11  5961  fununi  5962  imadif  5971  fnres  6005  mptfnf  6013  fnopabg  6015  fun  6064  fin  6083  dff1o2  6140  brprcneu  6182  dffv2  6269  fsn  6399  f13dfv  6527  dff1o6  6528  isotr  6583  eqoprab2b  6710  porpss  6938  sucelon  7014  elxp6  7197  dfoprab3  7221  opiota  7226  fsplit  7279  poxp  7286  soxp  7287  suppvalbr  7296  brtpos2  7355  wfrlem5  7416  wfrfun  7422  tfrlem7  7476  dfer2  7740  eqer  7774  eqerOLD  7775  iiner  7816  uniinqs  7824  brecop  7837  eroveu  7839  erovlem  7840  mapval2  7884  ixpin  7930  boxriin  7947  brsdom  7975  xpcomco  8047  xpassen  8051  sbthlem9  8075  sbthlem10  8076  brsdom2  8081  ssenen  8131  unfi  8224  dffi3  8334  dfsup2  8347  infcllem  8390  axinf2  8534  zfinf2  8536  oemapso  8576  scottexs  8747  scott0s  8748  kardex  8754  karden  8755  dfac5lem1  8943  dfac5lem3  8945  kmlem15  8983  enfin2i  9140  fin23lem34  9165  brdom7disj  9350  fpwwe2lem12  9460  fpwwe2lem13  9461  axgroth5  9643  grothprim  9653  addsrpr  9893  mulsrpr  9894  mulgt0sr  9923  addcnsr  9953  mulcnsr  9954  ltresr  9958  axcnre  9982  1re  10036  ssxr  10104  infrenegsup  11003  nnwos  11752  zmin  11781  xrnemnf  11948  xrnepnf  11949  xmullem  12091  xmulcom  12093  xmulneg1  12096  xmulf  12099  xrinfmss2  12138  elfzuzb  12333  fzass4  12376  seqof  12853  hashbclem  13231  hashfacen  13233  xpcogend  13707  trclublem  13728  rexanre  14080  caubnd  14092  o1lo1  14262  rpnnen2lem12  14948  lcmcllem  15303  lcmftp  15343  lcmfunsnlem2  15347  isprm3  15390  prmreclem2  15615  4sqlem12  15654  isffth2  16570  fucinv  16627  lublecllem  16982  oduglb  17133  odulub  17135  issubm  17341  issubmd  17343  isnsg2  17618  oppgid  17780  symgfixf1  17851  pmtrrn2  17874  lsmdisjr  18091  lsmhash  18112  dprd0  18424  issrg  18501  dvdsrtr  18646  isirred2  18695  lss1d  18957  lspsolvlem  19136  lbsextlem2  19153  evlsval  19513  cnfldfunALT  19753  unocv  20018  iunocv  20019  gsumcom3  20199  mpt2matmul  20246  cpmidpmat  20672  tgval2  20754  fctop  20802  ppttop  20805  epttop  20807  cnnei  21080  2ndcctbss  21252  txuni2  21362  txbas  21364  ptbasin  21374  txdis1cn  21432  xkococnlem  21456  opnfbas  21640  fgcl  21676  fbasrn  21682  filuni  21683  cfinfil  21691  csdfil  21692  fin1aufil  21730  rnelfmlem  21750  fmfnfmlem3  21754  txflf  21804  xmeterval  22231  reconn  22625  iimulcl  22730  isclmp  22891  iscau3  23070  rrxmvallem  23181  minveclem3  23194  pmltpc  23213  ovolfcl  23229  ismbl  23288  dyaddisj  23358  iblre  23554  plyun0  23947  logfaclbnd  24941  lgslem3  25018  lgsdir2lem5  25048  ishpg  25645  usgrexmpllem  26146  nb3grpr2  26279  vtxd0nedgb  26378  wlk1walk  26529  wspthnonp  26738  wwlksn0s  26740  wlknwwlksninj  26769  wlkwwlkinj  26776  wwlksnndef  26794  wwlksnfi  26795  2wlkdlem8  26823  elwwlks2s3  26853  clwwlksnndef  26884  clwwlksf1  26910  3pthdlem1  27017  upgr4cycl4dv4e  27038  numclwwlkovf2  27202  frgrreg  27236  ajfval  27648  issh  28049  chcon2i  28307  chcon3i  28309  spanuni  28387  5oalem7  28503  3oalem3  28507  pjin2i  29036  pjin3i  29037  cvnbtwn4  29132  mdslj1i  29162  mdslj2i  29163  mdslmd1i  29172  chrelat4i  29216  chirredi  29237  cdj3i  29284  difrab2  29323  iuninc  29363  fcoinvbr  29403  suppss2f  29423  fmptdF  29440  disjdsct  29465  cnvoprab  29483  f1od2  29484  tosglblem  29654  pmtrprfv2  29833  ordtconnlem1  29955  esumpfinvalf  30123  esum2dlem  30139  measiuns  30265  eulerpartlemt0  30416  eulerpartlemr  30421  eulerpartlemn  30428  ballotlem2  30535  ballotlemodife  30544  bnj887  30820  bnj976  30833  bnj1385  30888  bnj153  30935  bnj543  30948  bnj607  30971  bnj882  30981  bnj916  30988  bnj983  31006  derangenlem  31138  pconnconn  31198  elmpst  31418  dftr6  31626  dffr5  31629  dfpo2  31631  fundmpss  31650  elpotr  31670  soseq  31735  frrlem5  31768  frrlem5c  31770  nocvxmin  31878  sltrec  31908  brtxp  31971  brpprod  31976  brsset  31980  idsset  31981  dfon3  31983  ellimits  32001  dffun10  32005  elfuns  32006  brcart  32023  brimg  32028  brapply  32029  brcap  32031  brsuccf  32032  funpartfun  32034  dfrecs2  32041  dfrdg4  32042  altopthc  32062  altopthd  32063  altopelaltxp  32067  outsideoftr  32220  trer  32294  gtinfOLD  32298  neibastop1  32338  neifg  32350  df3nandALT1  32380  imnand2  32383  bj-eldiag2  33072  topdifinfeq  33178  relowlssretop  33191  relowlpssretop  33192  wl-cases2-dnf  33275  poimirlem30  33419  poimirlem32  33421  ismblfin  33430  mbfposadd  33437  inixp  33503  elghomOLD  33666  keridl  33811  smprngopr  33831  sbcani  33890  prtlem10  33976  prter1  33990  lcvbr3  34136  isopos  34293  llnexatN  34633  snatpsubN  34862  pclclN  35003  pclfinN  35012  lhpocnel2  35131  cdlemk19w  36086  dih1dimatlem  36444  mzpclall  37116  mzpincl  37123  mzpindd  37135  2nn0ind  37336  dford4  37422  wopprc  37423  islmodfg  37465  isdomn3  37608  ifpan123g  37629  ifpan23  37630  ifpdfbi  37644  ifpnot23  37649  ifpdfxor  37658  ifpidg  37662  ifpid1g  37665  ifpim23g  37666  ifpim123g  37671  ifpim1g  37672  ifp1bi  37673  ifpimimb  37675  ifpororb  37676  ifpor123g  37679  ifpbibib  37681  rp-isfinite6  37690  undmrnresiss  37736  cotrintab  37747  brtrclfv2  37845  dfxor4  37884  snhesn  37906  dffrege76  38059  uneqsn  38147  nzin  38343  onfrALTlem5  38583  onfrALTlem4  38584  undif3VD  38944  onfrALTlem5VD  38947  onfrALTlem4VD  38948  ndisj2  39044  rexabsle  39465  ellimcabssub0  39655  limsupre2mpt  39768  limsupre3  39771  limsupre3mpt  39772  limsupre3uz  39774  limsupreuz  39775  liminfreuz  39835  fourierdlem103  40195  fourierdlem104  40196  fourierdlem112  40204  smflim  40754  smflim2  40781  smflimsuplem1  40795  smflimsup  40803  2reu5a  40946  2reu1  40955  2reu4a  40958  issubmgm  41560  rabsubmgmd  41562  2zlidl  41705  mndpsuppss  41923  islininds2  42044  zlmodzxzldeplem3  42062  alsi-no-surprise  42313
  Copyright terms: Public domain W3C validator