Theorem anbi12i 464

Description: Conjoin both sides of two equivalences. (Contributed by NM, 5-Aug-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 462	. 2 |- ( ( ph /\ ch ) <-> ( ps /\ ch ) )
3		anbi12.2	. . 3 |- ( ch <-> th )
4	3	anbi2i 461	. 2 |- ( ( ps /\ ch ) <-> ( ps /\ th ) )
5	2, 4	bitri 184	1 |- ( ( ph /\ ch ) <-> ( ps /\ th ) )

This proof depends on syntax axioms:   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  anbi12ci  465  ordir  829  orddi  832  3anbi123i  1219  an6  1362  xorcom  1437  trubifal  1465  truxortru  1468  truxorfal  1469  falxortru  1470  falxorfal  1471  nford  1620  nfand  1621  sbequ8  1900  sbanv  1944  sban  2015  sbbi  2019  sbnf2  2041  eu1  2111  2exeu  2179  2eu4  2180  sbabel  2419  neanior  2507  rexeqbii  2563  r19.26m  2682  reean  2720  reu5  2770  cbvreuw  2781  reu2  3014  reu3  3016  eqss  3263  unss  3403  ralunb  3410  ssin  3453  undi  3479  difundi  3483  indifdir  3487  inab  3499  difab  3500  reuss2  3513  reupick  3517  raaan  3633  prss  3871  tpss  3883  prsspw  3890  prneimg  3899  uniin  3955  intun  4001  intpr  4002  disjiun  4125  brin  4184  brdif  4185  ssext  4363  pweqb  4365  opthg2  4381  copsex4g  4389  opelopabsb  4404  eqopab2b  4424  pwin  4429  pofun  4459  wetrep  4507  ordwe  4725  wessep  4727  reg3exmidlemwe  4728  elxp3  4831  soinxp  4847  relun  4896  inopab  4914  difopab  4915  inxp  4916  opelco2g  4950  cnvco  4967  dmin  4991  restidsing  5122  intasym  5175  asymref  5176  cnvdif  5197  xpm  5212  xp11m  5229  dfco2  5290  relssdmrn  5311  cnvpom  5333  xpcom  5337  dffun4  5391  dffun4f  5396  funun  5425  funcnveq  5447  fun11  5451  fununi  5452  imadif  5464  imainlem  5465  imain  5466  fnres  5503  fnopabg  5510  fun  5564  fin  5581  dff1o2  5647  brprcneu  5691  fsn  5883  dff1o6  5985  isotr  6025  brabvv  6137  eqoprab2b  6149  fvmpopr2d  6228  dfoprab3  6429  poxp  6472  cnvoprab  6474  f1od2  6475  brtpos2  6527  tfrlem7  6593  dfer2  6813  eqer  6844  iinerm  6886  brecop  6904  eroveu  6905  erovlem  6906  oviec  6920  mapval2  6964  ixpin  7011  modom  7114  xpcomco  7130  xpassen  7134  ssenen  7158  sbthlemi10  7290  infmoti  7374  dfmq0qs  7802  dfplq0qs  7803  enq0enq  7804  enq0tr  7807  npsspw  7844  nqprdisj  7917  ltnqpr  7966  ltnqpri  7967  ltexprlemdisj  7979  addcanprg  7989  recexprlemdisj  8003  caucvgprprlemval  8061  addsrpr  8118  mulsrpr  8119  mulgt0sr  8151  addcnsr  8207  mulcnsr  8208  ltresr  8212  addvalex  8217  axcnre  8254  axpre-suploc  8275  supinfneg  10010  infsupneg  10011  xrnemnf  10195  xrnepnf  10196  elfzuzb  10438  fzass4  10484  infssuzex  10682  hashfibclem  11303  hashfacen  11305  rexanre  12008  cbvprod  12349  nnwosdc  12840  isprm3  12920  issubm  13837  issubmd  13839  0subm  13849  insubm  13850  isnsg2  14064  lss1d  14828  tgval2  15294  epttop  15333  cnnei  15475  txuni2  15499  txbas  15501  txdis1cn  15521  xmeterval  15678  dedekindicc  15876  plyun0  15979  lgslem3  16343  vtxd0nedgbfi  16762  wlk1walkdom  16822  clwwlknonccat  16896  clwwlknon2x  16898  bj-stan  16997  nnti  17244  dfrals2  17354  alsbii  17365  ralsbii  17366  cbvals  17370  rals-no-surprise  17372  dfralseu2  17388  alseubii  17397  ralseubii  17398