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  824  orddi  827  3anbi123i  1214  an6  1357  xorcom  1432  trubifal  1460  truxortru  1463  truxorfal  1464  falxortru  1465  falxorfal  1466  nford  1615  nfand  1616  sbequ8  1894  sbanv  1937  sban  2007  sbbi  2011  sbnf2  2033  eu1  2103  2exeu  2171  2eu4  2172  sbabel  2400  neanior  2488  rexeqbii  2544  r19.26m  2663  reean  2701  reu5  2750  cbvreuw  2761  reu2  2993  reu3  2995  eqss  3241  unss  3380  ralunb  3387  ssin  3428  undi  3454  difundi  3458  indifdir  3462  inab  3474  difab  3475  reuss2  3486  reupick  3490  raaan  3599  prss  3828  tpss  3840  prsspw  3847  prneimg  3856  uniin  3912  intun  3958  intpr  3959  disjiun  4082  brin  4140  brdif  4141  ssext  4312  pweqb  4314  opthg2  4330  copsex4g  4338  opelopabsb  4353  eqopab2b  4373  pwin  4378  pofun  4408  wetrep  4456  ordwe  4673  wessep  4675  reg3exmidlemwe  4676  elxp3  4779  soinxp  4795  relun  4843  inopab  4861  difopab  4862  inxp  4863  opelco2g  4897  cnvco  4914  dmin  4938  restidsing  5068  intasym  5120  asymref  5121  cnvdif  5142  xpm  5157  xp11m  5174  dfco2  5235  relssdmrn  5256  cnvpom  5278  xpcom  5282  dffun4  5336  dffun4f  5341  funun  5370  funcnveq  5392  fun11  5396  fununi  5397  imadif  5409  imainlem  5410  imain  5411  fnres  5448  fnopabg  5455  fun  5507  fin  5522  dff1o2  5588  brprcneu  5632  fsn  5819  dff1o6  5919  isotr  5959  brabvv  6069  eqoprab2b  6081  fvmpopr2d  6160  dfoprab3  6356  poxp  6399  cnvoprab  6401  f1od2  6402  brtpos2  6419  tfrlem7  6485  dfer2  6705  eqer  6736  iinerm  6778  brecop  6796  eroveu  6797  erovlem  6798  oviec  6812  mapval2  6849  ixpin  6894  modom  6996  xpcomco  7012  xpassen  7016  ssenen  7039  sbthlemi10  7167  infmoti  7229  dfmq0qs  7651  dfplq0qs  7652  enq0enq  7653  enq0tr  7656  npsspw  7693  nqprdisj  7766  ltnqpr  7815  ltnqpri  7816  ltexprlemdisj  7828  addcanprg  7838  recexprlemdisj  7852  caucvgprprlemval  7910  addsrpr  7967  mulsrpr  7968  mulgt0sr  8000  addcnsr  8056  mulcnsr  8057  ltresr  8061  addvalex  8066  axcnre  8103  axpre-suploc  8124  supinfneg  9831  infsupneg  9832  xrnemnf  10014  xrnepnf  10015  elfzuzb  10256  fzass4  10299  infssuzex  10496  hashfacen  11103  rexanre  11800  cbvprod  12139  nnwosdc  12630  isprm3  12710  issubm  13575  issubmd  13577  0subm  13587  insubm  13588  isnsg2  13810  lss1d  14418  tgval2  14801  epttop  14840  cnnei  14982  txuni2  15006  txbas  15008  txdis1cn  15028  xmeterval  15185  dedekindicc  15383  plyun0  15486  lgslem3  15757  vtxd0nedgbfi  16176  wlk1walkdom  16236  clwwlknonccat  16310  clwwlknon2x  16312  bj-stan  16401  nnti  16649