Theorem anbi12i 460

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 458	. 2 |- ( ( ph /\ ch ) <-> ( ps /\ ch ) )
3		anbi12.2	. . 3 |- ( ch <-> th )
4	3	anbi2i 457	. 2 |- ( ( ps /\ ch ) <-> ( ps /\ th ) )
5	2, 4	bitri 184	1 |- ( ( ph /\ ch ) <-> ( ps /\ th ) )

Syntax hints:   /\ wa 104   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  anbi12ci  461  ordir  825  orddi  828  3anbi123i  1215  an6  1358  xorcom  1433  trubifal  1461  truxortru  1464  truxorfal  1465  falxortru  1466  falxorfal  1467  nford  1616  nfand  1617  sbequ8  1896  sbanv  1940  sban  2011  sbbi  2015  sbnf2  2037  eu1  2107  2exeu  2175  2eu4  2176  sbabel  2413  neanior  2501  rexeqbii  2557  r19.26m  2676  reean  2714  reu5  2764  cbvreuw  2775  reu2  3007  reu3  3009  eqss  3255  unss  3395  ralunb  3402  ssin  3445  undi  3471  difundi  3475  indifdir  3479  inab  3491  difab  3492  reuss2  3503  reupick  3507  raaan  3617  prss  3852  tpss  3864  prsspw  3871  prneimg  3880  uniin  3936  intun  3982  intpr  3983  disjiun  4106  brin  4164  brdif  4165  ssext  4339  pweqb  4341  opthg2  4357  copsex4g  4365  opelopabsb  4380  eqopab2b  4400  pwin  4405  pofun  4435  wetrep  4483  ordwe  4700  wessep  4702  reg3exmidlemwe  4703  elxp3  4806  soinxp  4822  relun  4871  inopab  4889  difopab  4890  inxp  4891  opelco2g  4925  cnvco  4942  dmin  4966  restidsing  5096  intasym  5149  asymref  5150  cnvdif  5171  xpm  5186  xp11m  5203  dfco2  5264  relssdmrn  5285  cnvpom  5307  xpcom  5311  dffun4  5365  dffun4f  5370  funun  5399  funcnveq  5421  fun11  5425  fununi  5426  imadif  5438  imainlem  5439  imain  5440  fnres  5477  fnopabg  5484  fun  5538  fin  5555  dff1o2  5621  brprcneu  5665  fsn  5851  dff1o6  5951  isotr  5991  brabvv  6101  eqoprab2b  6113  fvmpopr2d  6192  dfoprab3  6387  poxp  6430  cnvoprab  6432  f1od2  6433  brtpos2  6484  tfrlem7  6550  dfer2  6770  eqer  6801  iinerm  6843  brecop  6861  eroveu  6862  erovlem  6863  oviec  6877  mapval2  6914  ixpin  6960  modom  7063  xpcomco  7079  xpassen  7083  ssenen  7107  sbthlemi10  7238  infmoti  7321  dfmq0qs  7746  dfplq0qs  7747  enq0enq  7748  enq0tr  7751  npsspw  7788  nqprdisj  7861  ltnqpr  7910  ltnqpri  7911  ltexprlemdisj  7923  addcanprg  7933  recexprlemdisj  7947  caucvgprprlemval  8005  addsrpr  8062  mulsrpr  8063  mulgt0sr  8095  addcnsr  8151  mulcnsr  8152  ltresr  8156  addvalex  8161  axcnre  8198  axpre-suploc  8219  supinfneg  9930  infsupneg  9931  xrnemnf  10113  xrnepnf  10114  elfzuzb  10356  fzass4  10399  infssuzex  10597  hashfibclem  11210  hashfacen  11212  rexanre  11909  cbvprod  12248  nnwosdc  12739  isprm3  12819  issubm  13702  issubmd  13704  0subm  13714  insubm  13715  isnsg2  13937  lss1d  14548  tgval2  14933  epttop  14972  cnnei  15114  txuni2  15138  txbas  15140  txdis1cn  15160  xmeterval  15317  dedekindicc  15515  plyun0  15618  lgslem3  15892  vtxd0nedgbfi  16311  wlk1walkdom  16371  clwwlknonccat  16445  clwwlknon2x  16447  bj-stan  16536  nnti  16783