Theorem anbi12i 733

Description: Conjoin both sides of two equivalences. (Contributed by NM, 12-Mar-1993.)

Hypotheses

Ref	Expression
anbi12.1	|- ( ph <-> ps )
anbi12.2	|- ( ch <-> th )

Assertion

Ref	Expression
anbi12i	|- ( ( ph /\ ch ) <-> ( ps /\ th ) )

Proof of Theorem anbi12i

Step	Hyp	Ref	Expression
1		anbi12.1	. . 3 |- ( ph <-> ps )
2	1	anbi1i 731	. 2 |- ( ( ph /\ ch ) <-> ( ps /\ ch ) )
3		anbi12.2	. . 3 |- ( ch <-> th )
4	3	anbi2i 730	. 2 |- ( ( ps /\ ch ) <-> ( ps /\ th ) )
5	2, 4	bitri 264	1 |- ( ( ph /\ ch ) <-> ( ps /\ th ) )

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  1251  an6  1408  nanbi  1454  cadan  1548  nic-axALT  1599  19.43OLD  1811  sbequ8  1885  sbbi  2401  sbnf2  2439  2mo2  2550  2eu4  2556  sbabel  2793  neanior  2886  rexeqbii  3054  r19.26m  3067  reean  3106  2ralor  3109  reu5  3159  reu2  3394  reu3  3396  2reu5lem3  3415  eqss  3618  unss  3787  ralunb  3794  ssin  3835  undi  3874  indifdir  3883  undif3  3888  undif3OLD  3889  inab  3895  difab  3896  reuss2  3907  reupick  3911  ssdifsn  4318  prssOLD  4352  sstp  4367  tpss  4368  prneimg  4388  prnebg  4389  uniin  4457  intun  4509  intpr  4510  disjiun  4640  disjxiun  4649  disjxiunOLD  4650  brin  4704  brdif  4705  ssext  4923  pweqb  4925  opthg2  4948  copsex4g  4959  propeqop  4970  eqopab2b  5005  pwin  5018  pofun  5051  wetrep  5107  elxp3  5169  soinxp  5183  weinxp  5186  csbxp  5200  relun  5235  inopab  5252  difopab  5253  inxp  5254  opelco2g  5289  cnvco  5308  dmin  5332  restidsing  5458  intasym  5511  asymref  5512  asymref2  5513  cnvdif  5539  xpnz  5553  difxp  5558  xpdifid  5562  xp11  5569  dfco2  5634  relssdmrn  5656  cnvpo  5673  cnvso  5674  xpco  5675  dffun4  5900  funun  5932  fun11  5963  fununi  5964  imadif  5973  fnres  6007  mptfnf  6015  fnopabg  6017  fun  6066  fin  6085  dff1o2  6142  brprcneu  6184  dffv2  6271  fsn  6402  f13dfv  6530  dff1o6  6531  isotr  6586  eqoprab2b  6713  porpss  6941  sucelon  7017  elxp6  7200  dfoprab3  7224  opiota  7229  fsplit  7282  poxp  7289  soxp  7290  suppvalbr  7299  brtpos2  7358  wfrlem5  7419  wfrfun  7425  tfrlem7  7479  dfer2  7743  eqer  7777  eqerOLD  7778  iiner  7819  uniinqs  7827  brecop  7840  eroveu  7842  erovlem  7843  mapval2  7887  ixpin  7933  boxriin  7950  brsdom  7978  xpcomco  8050  xpassen  8054  sbthlem9  8078  sbthlem10  8079  brsdom2  8084  ssenen  8134  unfi  8227  dffi3  8337  dfsup2  8350  infcllem  8393  axinf2  8537  zfinf2  8539  oemapso  8579  scottexs  8750  scott0s  8751  kardex  8757  karden  8758  dfac5lem1  8946  dfac5lem3  8948  kmlem15  8986  enfin2i  9143  fin23lem34  9168  brdom7disj  9353  fpwwe2lem12  9463  fpwwe2lem13  9464  axgroth5  9646  grothprim  9656  addsrpr  9896  mulsrpr  9897  mulgt0sr  9926  addcnsr  9956  mulcnsr  9957  ltresr  9961  axcnre  9985  1re  10039  ssxr  10107  infrenegsup  11006  nnwos  11755  zmin  11784  xrnemnf  11951  xrnepnf  11952  xmullem  12094  xmulcom  12096  xmulneg1  12099  xmulf  12102  xrinfmss2  12141  elfzuzb  12336  fzass4  12379  seqof  12858  hashbclem  13236  hashfacen  13238  xpcogend  13713  trclublem  13734  rexanre  14086  caubnd  14098  o1lo1  14268  rpnnen2lem12  14954  lcmcllem  15309  lcmftp  15349  lcmfunsnlem2  15353  isprm3  15396  prmreclem2  15621  4sqlem12  15660  isffth2  16576  fucinv  16633  lublecllem  16988  oduglb  17139  odulub  17141  issubm  17347  issubmd  17349  isnsg2  17624  oppgid  17786  symgfixf1  17857  pmtrrn2  17880  lsmdisjr  18097  lsmhash  18118  dprd0  18430  issrg  18507  dvdsrtr  18652  isirred2  18701  lss1d  18963  lspsolvlem  19142  lbsextlem2  19159  evlsval  19519  cnfldfunALT  19759  unocv  20024  iunocv  20025  gsumcom3  20205  mpt2matmul  20252  cpmidpmat  20678  tgval2  20760  fctop  20808  ppttop  20811  epttop  20813  cnnei  21086  2ndcctbss  21258  txuni2  21368  txbas  21370  ptbasin  21380  txdis1cn  21438  xkococnlem  21462  opnfbas  21646  fgcl  21682  fbasrn  21688  filuni  21689  cfinfil  21697  csdfil  21698  fin1aufil  21736  rnelfmlem  21756  fmfnfmlem3  21760  txflf  21810  xmeterval  22237  reconn  22631  iimulcl  22736  isclmp  22897  iscau3  23076  rrxmvallem  23187  minveclem3  23200  pmltpc  23219  ovolfcl  23235  ismbl  23294  dyaddisj  23364  iblre  23560  plyun0  23953  logfaclbnd  24947  lgslem3  25024  lgsdir2lem5  25054  ishpg  25651  usgrexmpllem  26152  nb3grpr2  26285  vtxd0nedgb  26384  wlk1walk  26535  wspthnonp  26744  wwlksn0s  26746  wlknwwlksninj  26775  wlkwwlkinj  26782  wwlksnndef  26800  wwlksnfi  26801  2wlkdlem8  26829  elwwlks2s3  26859  clwwlksnndef  26890  clwwlksf1  26917  3pthdlem1  27024  upgr4cycl4dv4e  27045  numclwwlkovf2  27217  frgrreg  27252  ajfval  27664  issh  28065  chcon2i  28323  chcon3i  28325  spanuni  28403  5oalem7  28519  3oalem3  28523  pjin2i  29052  pjin3i  29053  cvnbtwn4  29148  mdslj1i  29178  mdslj2i  29179  mdslmd1i  29188  chrelat4i  29232  chirredi  29253  cdj3i  29300  difrab2  29339  iuninc  29379  fcoinvbr  29419  suppss2f  29439  fmptdF  29456  disjdsct  29480  cnvoprab  29498  f1od2  29499  tosglblem  29669  pmtrprfv2  29848  ordtconnlem1  29970  esumpfinvalf  30138  esum2dlem  30154  measiuns  30280  eulerpartlemt0  30431  eulerpartlemr  30436  eulerpartlemn  30443  ballotlem2  30550  ballotlemodife  30559  bnj887  30835  bnj976  30848  bnj1385  30903  bnj153  30950  bnj543  30963  bnj607  30986  bnj882  30996  bnj916  31003  bnj983  31021  derangenlem  31153  pconnconn  31213  elmpst  31433  dftr6  31640  dffr5  31643  dfpo2  31645  fundmpss  31664  elpotr  31686  soseq  31751  frrlem5  31784  frrlem5c  31786  nocvxmin  31894  sltrec  31924  brtxp  31987  brpprod  31992  brsset  31996  idsset  31997  dfon3  31999  ellimits  32017  dffun10  32021  elfuns  32022  brcart  32039  brimg  32044  brapply  32045  brcap  32047  brsuccf  32048  funpartfun  32050  dfrecs2  32057  dfrdg4  32058  altopthc  32078  altopthd  32079  altopelaltxp  32083  outsideoftr  32236  trer  32310  gtinfOLD  32314  neibastop1  32354  neifg  32366  df3nandALT1  32396  imnand2  32399  bj-eldiag2  33092  topdifinfeq  33198  relowlssretop  33211  relowlpssretop  33212  wl-cases2-dnf  33295  poimirlem30  33439  poimirlem32  33441  ismblfin  33450  mbfposadd  33457  inixp  33523  elghomOLD  33686  keridl  33831  smprngopr  33851  sbcani  33910  an2anr  33998  prtlem10  34150  prter1  34164  lcvbr3  34310  isopos  34467  llnexatN  34807  snatpsubN  35036  pclclN  35177  pclfinN  35186  lhpocnel2  35305  cdlemk19w  36260  dih1dimatlem  36618  mzpclall  37290  mzpincl  37297  mzpindd  37309  2nn0ind  37510  dford4  37596  wopprc  37597  islmodfg  37639  isdomn3  37782  ifpan123g  37803  ifpan23  37804  ifpdfbi  37818  ifpnot23  37823  ifpdfxor  37832  ifpidg  37836  ifpid1g  37839  ifpim23g  37840  ifpim123g  37845  ifpim1g  37846  ifp1bi  37847  ifpimimb  37849  ifpororb  37850  ifpor123g  37853  ifpbibib  37855  rp-isfinite6  37864  undmrnresiss  37910  cotrintab  37921  brtrclfv2  38019  dfxor4  38058  snhesn  38080  dffrege76  38233  uneqsn  38321  nzin  38517  onfrALTlem5  38757  onfrALTlem4  38758  undif3VD  39118  onfrALTlem5VD  39121  onfrALTlem4VD  39122  ndisj2  39218  rexabsle  39646  ellimcabssub0  39849  limsupre2mpt  39962  limsupre3  39965  limsupre3mpt  39966  limsupre3uz  39968  limsupreuz  39969  liminfreuz  40035  fourierdlem103  40426  fourierdlem104  40427  fourierdlem112  40435  smflim  40985  smflim2  41012  smflimsuplem1  41026  smflimsup  41034  2reu5a  41177  2reu1  41186  2reu4a  41189  issubmgm  41789  rabsubmgmd  41791  2zlidl  41934  mndpsuppss  42152  islininds2  42273  zlmodzxzldeplem3  42291  alsi-no-surprise  42542