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  6526  tfrlem7  6592  dfer2  6812  eqer  6843  iinerm  6885  brecop  6903  eroveu  6904  erovlem  6905  oviec  6919  mapval2  6963  ixpin  7009  modom  7112  xpcomco  7128  xpassen  7132  ssenen  7156  sbthlemi10  7288  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  10011  infsupneg  10012  xrnemnf  10196  xrnepnf  10197  elfzuzb  10439  fzass4  10485  infssuzex  10683  hashfibclem  11304  hashfacen  11306  rexanre  12009  cbvprod  12350  nnwosdc  12841  isprm3  12921  issubm  13838  issubmd  13840  0subm  13850  insubm  13851  isnsg2  14065  lss1d  14829  tgval2  15277  epttop  15316  cnnei  15458  txuni2  15482  txbas  15484  txdis1cn  15504  xmeterval  15661  dedekindicc  15859  plyun0  15962  lgslem3  16326  vtxd0nedgbfi  16745  wlk1walkdom  16805  clwwlknonccat  16879  clwwlknon2x  16881  bj-stan  16980  nnti  17227  dfrals2  17337  alsbii  17348  ralsbii  17349  cbvals  17353  rals-no-surprise  17355  dfralseu2  17371  alseubii  17380  ralseubii  17381