Theorem anbi12i 456

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  anbi12ci  457  ordir  807  orddi  810  dcan  919  3anbi123i  1171  an6  1300  xorcom  1367  trubifal  1395  truxortru  1398  truxorfal  1399  falxortru  1400  falxorfal  1401  nford  1547  nfand  1548  sbequ8  1820  sbanv  1862  sban  1929  sbbi  1933  sbnf2  1957  eu1  2025  2exeu  2092  2eu4  2093  sbabel  2308  neanior  2396  rexeqbii  2451  r19.26m  2566  reean  2602  reu5  2646  reu2  2876  reu3  2878  eqss  3117  unss  3255  ralunb  3262  ssin  3303  undi  3329  difundi  3333  indifdir  3337  inab  3349  difab  3350  reuss2  3361  reupick  3365  raaan  3474  prss  3684  tpss  3693  prsspw  3700  prneimg  3709  uniin  3764  intun  3810  intpr  3811  disjiun  3932  brin  3988  brdif  3989  ssext  4151  pweqb  4153  opthg2  4169  copsex4g  4177  opelopabsb  4190  eqopab2b  4209  pwin  4212  pofun  4242  wetrep  4290  ordwe  4498  wessep  4500  reg3exmidlemwe  4501  elxp3  4601  soinxp  4617  relun  4664  inopab  4679  difopab  4680  inxp  4681  opelco2g  4715  cnvco  4732  dmin  4755  intasym  4931  asymref  4932  cnvdif  4953  xpm  4968  xp11m  4985  dfco2  5046  relssdmrn  5067  cnvpom  5089  xpcom  5093  dffun4  5142  dffun4f  5147  funun  5175  funcnveq  5194  fun11  5198  fununi  5199  imadif  5211  imainlem  5212  imain  5213  fnres  5247  fnopabg  5254  fun  5303  fin  5317  dff1o2  5380  brprcneu  5422  fsn  5600  dff1o6  5685  isotr  5725  brabvv  5825  eqoprab2b  5837  dfoprab3  6097  poxp  6137  cnvoprab  6139  f1od2  6140  brtpos2  6156  tfrlem7  6222  dfer2  6438  eqer  6469  iinerm  6509  brecop  6527  eroveu  6528  erovlem  6529  oviec  6543  mapval2  6580  ixpin  6625  xpcomco  6728  xpassen  6732  ssenen  6753  sbthlemi10  6862  infmoti  6923  dfmq0qs  7261  dfplq0qs  7262  enq0enq  7263  enq0tr  7266  npsspw  7303  nqprdisj  7376  ltnqpr  7425  ltnqpri  7426  ltexprlemdisj  7438  addcanprg  7448  recexprlemdisj  7462  caucvgprprlemval  7520  addsrpr  7577  mulsrpr  7578  mulgt0sr  7610  addcnsr  7666  mulcnsr  7667  ltresr  7671  addvalex  7676  axcnre  7713  axpre-suploc  7734  supinfneg  9417  infsupneg  9418  xrnemnf  9594  xrnepnf  9595  elfzuzb  9831  fzass4  9873  hashfacen  10611  rexanre  11024  cbvprod  11359  infssuzex  11678  isprm3  11835  tgval2  12259  epttop  12298  cnnei  12440  txuni2  12464  txbas  12466  txdis1cn  12486  xmeterval  12643  dedekindicc  12819  bj-stan  13126  nnti  13362