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  1895  sbanv  1938  sban  2008  sbbi  2012  sbnf2  2034  eu1  2104  2exeu  2172  2eu4  2173  sbabel  2402  neanior  2490  rexeqbii  2546  r19.26m  2665  reean  2703  reu5  2752  cbvreuw  2763  reu2  2995  reu3  2997  eqss  3243  unss  3383  ralunb  3390  ssin  3431  undi  3457  difundi  3461  indifdir  3465  inab  3477  difab  3478  reuss2  3489  reupick  3493  raaan  3602  prss  3834  tpss  3846  prsspw  3853  prneimg  3862  uniin  3918  intun  3964  intpr  3965  disjiun  4088  brin  4146  brdif  4147  ssext  4319  pweqb  4321  opthg2  4337  copsex4g  4345  opelopabsb  4360  eqopab2b  4380  pwin  4385  pofun  4415  wetrep  4463  ordwe  4680  wessep  4682  reg3exmidlemwe  4683  elxp3  4786  soinxp  4802  relun  4850  inopab  4868  difopab  4869  inxp  4870  opelco2g  4904  cnvco  4921  dmin  4945  restidsing  5075  intasym  5128  asymref  5129  cnvdif  5150  xpm  5165  xp11m  5182  dfco2  5243  relssdmrn  5264  cnvpom  5286  xpcom  5290  dffun4  5344  dffun4f  5349  funun  5378  funcnveq  5400  fun11  5404  fununi  5405  imadif  5417  imainlem  5418  imain  5419  fnres  5456  fnopabg  5463  fun  5516  fin  5531  dff1o2  5597  brprcneu  5641  fsn  5827  dff1o6  5927  isotr  5967  brabvv  6077  eqoprab2b  6089  fvmpopr2d  6168  dfoprab3  6363  poxp  6406  cnvoprab  6408  f1od2  6409  brtpos2  6460  tfrlem7  6526  dfer2  6746  eqer  6777  iinerm  6819  brecop  6837  eroveu  6838  erovlem  6839  oviec  6853  mapval2  6890  ixpin  6935  modom  7037  xpcomco  7053  xpassen  7057  ssenen  7080  sbthlemi10  7208  infmoti  7287  dfmq0qs  7709  dfplq0qs  7710  enq0enq  7711  enq0tr  7714  npsspw  7751  nqprdisj  7824  ltnqpr  7873  ltnqpri  7874  ltexprlemdisj  7886  addcanprg  7896  recexprlemdisj  7910  caucvgprprlemval  7968  addsrpr  8025  mulsrpr  8026  mulgt0sr  8058  addcnsr  8114  mulcnsr  8115  ltresr  8119  addvalex  8124  axcnre  8161  axpre-suploc  8182  supinfneg  9890  infsupneg  9891  xrnemnf  10073  xrnepnf  10074  elfzuzb  10316  fzass4  10359  infssuzex  10556  hashfacen  11163  rexanre  11860  cbvprod  12199  nnwosdc  12690  isprm3  12770  issubm  13635  issubmd  13637  0subm  13647  insubm  13648  isnsg2  13870  lss1d  14479  tgval2  14862  epttop  14901  cnnei  15043  txuni2  15067  txbas  15069  txdis1cn  15089  xmeterval  15246  dedekindicc  15444  plyun0  15547  lgslem3  15821  vtxd0nedgbfi  16240  wlk1walkdom  16300  clwwlknonccat  16374  clwwlknon2x  16376  bj-stan  16465  nnti  16712