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  822  orddi  825  3anbi123i  1212  an6  1355  xorcom  1430  trubifal  1458  truxortru  1461  truxorfal  1462  falxortru  1463  falxorfal  1464  nford  1613  nfand  1614  sbequ8  1893  sbanv  1936  sban  2006  sbbi  2010  sbnf2  2032  eu1  2102  2exeu  2170  2eu4  2171  sbabel  2399  neanior  2487  rexeqbii  2543  r19.26m  2662  reean  2700  reu5  2749  cbvreuw  2760  reu2  2991  reu3  2993  eqss  3239  unss  3378  ralunb  3385  ssin  3426  undi  3452  difundi  3456  indifdir  3460  inab  3472  difab  3473  reuss2  3484  reupick  3488  raaan  3597  prss  3824  tpss  3836  prsspw  3843  prneimg  3852  uniin  3908  intun  3954  intpr  3955  disjiun  4078  brin  4136  brdif  4137  ssext  4307  pweqb  4309  opthg2  4325  copsex4g  4333  opelopabsb  4348  eqopab2b  4368  pwin  4373  pofun  4403  wetrep  4451  ordwe  4668  wessep  4670  reg3exmidlemwe  4671  elxp3  4773  soinxp  4789  relun  4836  inopab  4854  difopab  4855  inxp  4856  opelco2g  4890  cnvco  4907  dmin  4931  restidsing  5061  intasym  5113  asymref  5114  cnvdif  5135  xpm  5150  xp11m  5167  dfco2  5228  relssdmrn  5249  cnvpom  5271  xpcom  5275  dffun4  5329  dffun4f  5334  funun  5362  funcnveq  5384  fun11  5388  fununi  5389  imadif  5401  imainlem  5402  imain  5403  fnres  5440  fnopabg  5447  fun  5497  fin  5512  dff1o2  5577  brprcneu  5620  fsn  5807  dff1o6  5900  isotr  5940  brabvv  6050  eqoprab2b  6062  fvmpopr2d  6141  dfoprab3  6337  poxp  6378  cnvoprab  6380  f1od2  6381  brtpos2  6397  tfrlem7  6463  dfer2  6681  eqer  6712  iinerm  6754  brecop  6772  eroveu  6773  erovlem  6774  oviec  6788  mapval2  6825  ixpin  6870  xpcomco  6985  xpassen  6989  ssenen  7012  sbthlemi10  7133  infmoti  7195  dfmq0qs  7616  dfplq0qs  7617  enq0enq  7618  enq0tr  7621  npsspw  7658  nqprdisj  7731  ltnqpr  7780  ltnqpri  7781  ltexprlemdisj  7793  addcanprg  7803  recexprlemdisj  7817  caucvgprprlemval  7875  addsrpr  7932  mulsrpr  7933  mulgt0sr  7965  addcnsr  8021  mulcnsr  8022  ltresr  8026  addvalex  8031  axcnre  8068  axpre-suploc  8089  supinfneg  9790  infsupneg  9791  xrnemnf  9973  xrnepnf  9974  elfzuzb  10215  fzass4  10258  infssuzex  10453  hashfacen  11058  rexanre  11731  cbvprod  12069  nnwosdc  12560  isprm3  12640  issubm  13505  issubmd  13507  0subm  13517  insubm  13518  isnsg2  13740  lss1d  14347  tgval2  14725  epttop  14764  cnnei  14906  txuni2  14930  txbas  14932  txdis1cn  14952  xmeterval  15109  dedekindicc  15307  plyun0  15410  lgslem3  15681  wlk1walkdom  16070  bj-stan  16111  nnti  16356