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 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 197  df-an 385
This theorem is referenced by:  anbi12ci  734  ordi  926  ordir  927  orddi  931  pm5.17  950  xor  953  cases2  1016  3anbi123i  1270  an6  1448  nanbi  1494  cadan  1588  nic-axALT  1639  19.43OLD  1851  sbequ8  1942  sbbi  2429  sbnf2  2467  2mo2  2579  2eu4  2585  sbabel  2822  neanior  2915  rexeqbii  3083  r19.26m  3096  reean  3135  2ralor  3138  reu5  3189  reu2  3427  reu3  3429  2reu5lem3  3448  eqss  3651  unss  3820  ralunb  3827  ssin  3868  undi  3907  indifdir  3916  undif3  3921  undif3OLD  3922  inab  3928  difab  3929  reuss2  3940  reupick  3944  ssdifsn  4351  prssOLD  4384  sstp  4399  tpss  4400  prneimg  4419  prnebg  4420  uniin  4489  intun  4541  intpr  4542  disjiun  4672  disjxiun  4681  disjxiunOLD  4682  brin  4737  brdif  4738  ssext  4953  pweqb  4955  opthg2  4977  copsex4g  4988  propeqop  4999  eqopab2b  5034  pwin  5047  pofun  5080  wetrep  5136  elxp3  5203  soinxp  5217  weinxp  5220  csbxp  5234  relun  5268  inopab  5285  difopab  5286  inxp  5287  opelco2g  5322  cnvco  5340  dmin  5364  restidsing  5493  intasym  5546  asymref  5547  asymref2  5548  cnvdif  5574  xpnz  5588  difxp  5593  xpdifid  5597  xp11  5604  dfco2  5672  relssdmrn  5694  cnvpo  5711  cnvso  5712  xpco  5713  dffun4  5938  funun  5970  fun11  6001  fununi  6002  imadif  6011  fnres  6045  mptfnf  6053  fnopabg  6055  fun  6104  fin  6123  dff1o2  6180  brprcneu  6222  dffv2  6310  fsn  6442  f13dfv  6570  dff1o6  6571  isotr  6626  eqoprab2b  6755  porpss  6983  sucelon  7059  elxp6  7244  dfoprab3  7268  opiota  7273  fsplit  7327  poxp  7334  soxp  7335  suppvalbr  7344  brtpos2  7403  wfrlem5  7464  wfrfun  7470  tfrlem7  7524  dfer2  7788  eqer  7822  iiner  7862  uniinqs  7870  brecop  7883  eroveu  7885  erovlem  7886  mapval2  7929  ixpin  7975  boxriin  7992  brsdom  8020  xpcomco  8091  xpassen  8095  sbthlem9  8119  sbthlem10  8120  brsdom2  8125  ssenen  8175  unfi  8268  dffi3  8378  dfsup2  8391  infcllem  8434  axinf2  8575  zfinf2  8577  oemapso  8617  scottexs  8788  scott0s  8789  kardex  8795  karden  8796  dfac5lem1  8984  dfac5lem3  8986  kmlem15  9024  enfin2i  9181  fin23lem34  9206  brdom7disj  9391  fpwwe2lem12  9501  fpwwe2lem13  9502  axgroth5  9684  grothprim  9694  addsrpr  9934  mulsrpr  9935  mulgt0sr  9964  addcnsr  9994  mulcnsr  9995  ltresr  9999  axcnre  10023  1re  10077  ssxr  10145  infrenegsup  11044  nnwos  11793  zmin  11822  xrnemnf  11989  xrnepnf  11990  xmullem  12132  xmulcom  12134  xmulneg1  12137  xmulf  12140  xrinfmss2  12179  elfzuzb  12374  fzass4  12417  seqof  12898  hashbclem  13274  hashfacen  13276  xpcogend  13759  trclublem  13780  rexanre  14130  caubnd  14142  o1lo1  14312  rpnnen2lem12  14998  lcmcllem  15356  lcmftp  15396  lcmfunsnlem2  15400  isprm3  15443  prmreclem2  15668  4sqlem12  15707  isffth2  16623  fucinv  16680  lublecllem  17035  oduglb  17186  odulub  17188  issubm  17394  issubmd  17396  isnsg2  17671  oppgid  17832  symgfixf1  17903  pmtrrn2  17926  lsmdisjr  18143  lsmhash  18164  dprd0  18476  issrg  18553  dvdsrtr  18698  isirred2  18747  lss1d  19011  lspsolvlem  19190  lbsextlem2  19207  evlsval  19567  cnfldfunALT  19807  unocv  20072  iunocv  20073  gsumcom3  20253  mpt2matmul  20300  cpmidpmat  20726  tgval2  20808  fctop  20856  ppttop  20859  epttop  20861  cnnei  21134  2ndcctbss  21306  txuni2  21416  txbas  21418  ptbasin  21428  txdis1cn  21486  xkococnlem  21510  opnfbas  21693  fgcl  21729  fbasrn  21735  filuni  21736  cfinfil  21744  csdfil  21745  fin1aufil  21783  rnelfmlem  21803  fmfnfmlem3  21807  txflf  21857  xmeterval  22284  reconn  22678  iimulcl  22783  isclmp  22943  iscau3  23122  rrxmvallem  23233  minveclem3  23246  pmltpc  23265  ovolfcl  23281  ismbl  23340  dyaddisj  23410  iblre  23605  plyun0  23998  logfaclbnd  24992  lgslem3  25069  lgsdir2lem5  25099  ishpg  25696  usgrexmpllem  26197  nb3grpr2  26329  vtxd0nedgb  26440  wlk1walk  26591  wwlknllvtx  26795  wwlksonvtx  26805  wspthnonp  26813  wwlksn0s  26815  wlknwwlksninj  26843  wlkwwlkinj  26850  wwlksnndef  26868  wwlksnfi  26869  2wlkdlem8  26898  elwwlks2s3  26916  clwwlkf1  27012  clwwlknon2x  27078  3pthdlem1  27142  upgr4cycl4dv4e  27163  frgr2wwlk1  27309  clwwlknonccat  27334  frgrreg  27381  ajfval  27792  issh  28193  chcon2i  28451  chcon3i  28453  spanuni  28531  5oalem7  28647  3oalem3  28651  pjin2i  29180  pjin3i  29181  cvnbtwn4  29276  mdslj1i  29306  mdslj2i  29307  mdslmd1i  29316  chrelat4i  29360  chirredi  29381  cdj3i  29428  difrab2  29465  iuninc  29505  fcoinvbr  29545  suppss2f  29567  fmptdF  29584  disjdsct  29608  cnvoprabOLD  29626  f1od2  29627  tosglblem  29797  pmtrprfv2  29976  ordtconnlem1  30098  esumpfinvalf  30266  esum2dlem  30282  measiuns  30408  eulerpartlemt0  30559  eulerpartlemr  30564  eulerpartlemn  30571  ballotlem2  30678  ballotlemodife  30687  bnj887  30961  bnj976  30974  bnj1385  31029  bnj153  31076  bnj543  31089  bnj607  31112  bnj882  31122  bnj916  31129  bnj983  31147  derangenlem  31279  pconnconn  31339  elmpst  31559  dftr6  31766  dffr5  31769  dfpo2  31771  fundmpss  31790  elpotr  31810  soseq  31879  frrlem5  31909  frrlem5c  31911  nocvxmin  32019  sltrec  32049  brtxp  32112  brpprod  32117  brsset  32121  idsset  32122  dfon3  32124  ellimits  32142  dffun10  32146  elfuns  32147  brcart  32164  brimg  32169  brapply  32170  brcap  32172  brsuccf  32173  funpartfun  32175  dfrecs2  32182  dfrdg4  32183  altopthc  32203  altopthd  32204  altopelaltxp  32208  outsideoftr  32361  trer  32435  gtinfOLD  32439  neibastop1  32479  neifg  32491  df3nandALT1  32521  imnand2  32524  bj-eldiag2  33222  topdifinfeq  33328  relowlssretop  33341  relowlpssretop  33342  wl-cases2-dnf  33425  poimirlem30  33569  poimirlem32  33571  ismblfin  33580  mbfposadd  33587  inixp  33653  elghomOLD  33816  keridl  33961  smprngopr  33981  sbcani  34040  an2anr  34141  inxpxrn  34293  dfcoss2  34311  1cossres  34324  dfcoels  34325  br1cossinres  34337  br1cossinidres  34339  br1cossincnvepres  34340  br1cossxrnidres  34341  br1cossxrncnvepres  34342  cosscnvssid3  34366  coss0  34369  cossid  34370  trcoss  34372  eleccossin  34373  dfssr2  34389  br1cossxrncnvssrres  34398  refsymrels3  34450  refsymrel2  34451  refsymrel3  34452  elrefsymrels3  34454  prtlem10  34469  prter1  34483  lcvbr3  34628  isopos  34785  llnexatN  35125  snatpsubN  35354  pclclN  35495  pclfinN  35504  lhpocnel2  35623  cdlemk19w  36577  dih1dimatlem  36935  mzpclall  37607  mzpincl  37614  mzpindd  37626  2nn0ind  37827  dford4  37913  wopprc  37914  islmodfg  37956  isdomn3  38099  ifpan123g  38120  ifpan23  38121  ifpdfbi  38135  ifpnot23  38140  ifpdfxor  38149  ifpidg  38153  ifpid1g  38156  ifpim23g  38157  ifpim123g  38162  ifpim1g  38163  ifp1bi  38164  ifpimimb  38166  ifpororb  38167  ifpor123g  38170  ifpbibib  38172  rp-isfinite6  38181  undmrnresiss  38227  cotrintab  38238  brtrclfv2  38336  dfxor4  38375  snhesn  38397  dffrege76  38550  uneqsn  38638  nzin  38834  onfrALTlem5  39074  onfrALTlem4  39075  undif3VD  39432  onfrALTlem5VD  39435  onfrALTlem4VD  39436  ndisj2  39532  rexabsle  39959  ellimcabssub0  40167  limsupre2mpt  40280  limsupre3  40283  limsupre3mpt  40284  limsupre3uz  40286  limsupreuz  40287  liminfreuz  40353  fourierdlem103  40744  fourierdlem104  40745  fourierdlem112  40753  smflim  41306  smflim2  41333  smflimsuplem1  41347  smflimsup  41355  2reu5a  41498  2reu1  41507  2reu4a  41510  issubmgm  42114  rabsubmgmd  42116  2zlidl  42259  mndpsuppss  42477  islininds2  42598  zlmodzxzldeplem3  42616  alsi-no-surprise  42870
  Copyright terms: Public domain W3C validator