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  818  orddi  821  3anbi123i  1190  an6  1332  xorcom  1399  trubifal  1427  truxortru  1430  truxorfal  1431  falxortru  1432  falxorfal  1433  nford  1581  nfand  1582  sbequ8  1861  sbanv  1904  sban  1974  sbbi  1978  sbnf2  2000  eu1  2070  2exeu  2137  2eu4  2138  sbabel  2366  neanior  2454  rexeqbii  2510  r19.26m  2628  reean  2666  reu5  2714  reu2  2952  reu3  2954  eqss  3199  unss  3338  ralunb  3345  ssin  3386  undi  3412  difundi  3416  indifdir  3420  inab  3432  difab  3433  reuss2  3444  reupick  3448  raaan  3557  prss  3779  tpss  3789  prsspw  3796  prneimg  3805  uniin  3860  intun  3906  intpr  3907  disjiun  4029  brin  4086  brdif  4087  ssext  4255  pweqb  4257  opthg2  4273  copsex4g  4281  opelopabsb  4295  eqopab2b  4315  pwin  4318  pofun  4348  wetrep  4396  ordwe  4613  wessep  4615  reg3exmidlemwe  4616  elxp3  4718  soinxp  4734  relun  4781  inopab  4799  difopab  4800  inxp  4801  opelco2g  4835  cnvco  4852  dmin  4875  restidsing  5003  intasym  5055  asymref  5056  cnvdif  5077  xpm  5092  xp11m  5109  dfco2  5170  relssdmrn  5191  cnvpom  5213  xpcom  5217  dffun4  5270  dffun4f  5275  funun  5303  funcnveq  5322  fun11  5326  fununi  5327  imadif  5339  imainlem  5340  imain  5341  fnres  5377  fnopabg  5384  fun  5433  fin  5447  dff1o2  5512  brprcneu  5554  fsn  5737  dff1o6  5826  isotr  5866  brabvv  5972  eqoprab2b  5984  fvmpopr2d  6063  dfoprab3  6258  poxp  6299  cnvoprab  6301  f1od2  6302  brtpos2  6318  tfrlem7  6384  dfer2  6602  eqer  6633  iinerm  6675  brecop  6693  eroveu  6694  erovlem  6695  oviec  6709  mapval2  6746  ixpin  6791  xpcomco  6894  xpassen  6898  ssenen  6921  sbthlemi10  7041  infmoti  7103  dfmq0qs  7513  dfplq0qs  7514  enq0enq  7515  enq0tr  7518  npsspw  7555  nqprdisj  7628  ltnqpr  7677  ltnqpri  7678  ltexprlemdisj  7690  addcanprg  7700  recexprlemdisj  7714  caucvgprprlemval  7772  addsrpr  7829  mulsrpr  7830  mulgt0sr  7862  addcnsr  7918  mulcnsr  7919  ltresr  7923  addvalex  7928  axcnre  7965  axpre-suploc  7986  supinfneg  9686  infsupneg  9687  xrnemnf  9869  xrnepnf  9870  elfzuzb  10111  fzass4  10154  infssuzex  10340  hashfacen  10945  rexanre  11402  cbvprod  11740  nnwosdc  12231  isprm3  12311  issubm  13174  issubmd  13176  0subm  13186  insubm  13187  isnsg2  13409  lss1d  14015  tgval2  14371  epttop  14410  cnnei  14552  txuni2  14576  txbas  14578  txdis1cn  14598  xmeterval  14755  dedekindicc  14953  plyun0  15056  lgslem3  15327  bj-stan  15477  nnti  15723