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  dcan  934  3anbi123i  1189  an6  1331  xorcom  1398  trubifal  1426  truxortru  1429  truxorfal  1430  falxortru  1431  falxorfal  1432  nford  1577  nfand  1578  sbequ8  1857  sbanv  1899  sban  1965  sbbi  1969  sbnf2  1991  eu1  2061  2exeu  2128  2eu4  2129  sbabel  2356  neanior  2444  rexeqbii  2500  r19.26m  2618  reean  2656  reu5  2700  reu2  2937  reu3  2939  eqss  3182  unss  3321  ralunb  3328  ssin  3369  undi  3395  difundi  3399  indifdir  3403  inab  3415  difab  3416  reuss2  3427  reupick  3431  raaan  3541  prss  3760  tpss  3770  prsspw  3777  prneimg  3786  uniin  3841  intun  3887  intpr  3888  disjiun  4010  brin  4067  brdif  4068  ssext  4233  pweqb  4235  opthg2  4251  copsex4g  4259  opelopabsb  4272  eqopab2b  4291  pwin  4294  pofun  4324  wetrep  4372  ordwe  4587  wessep  4589  reg3exmidlemwe  4590  elxp3  4692  soinxp  4708  relun  4755  inopab  4771  difopab  4772  inxp  4773  opelco2g  4807  cnvco  4824  dmin  4847  restidsing  4975  intasym  5025  asymref  5026  cnvdif  5047  xpm  5062  xp11m  5079  dfco2  5140  relssdmrn  5161  cnvpom  5183  xpcom  5187  dffun4  5239  dffun4f  5244  funun  5272  funcnveq  5291  fun11  5295  fununi  5296  imadif  5308  imainlem  5309  imain  5310  fnres  5344  fnopabg  5351  fun  5400  fin  5414  dff1o2  5478  brprcneu  5520  fsn  5701  dff1o6  5790  isotr  5830  brabvv  5934  eqoprab2b  5946  dfoprab3  6206  poxp  6247  cnvoprab  6249  f1od2  6250  brtpos2  6266  tfrlem7  6332  dfer2  6550  eqer  6581  iinerm  6621  brecop  6639  eroveu  6640  erovlem  6641  oviec  6655  mapval2  6692  ixpin  6737  xpcomco  6840  xpassen  6844  ssenen  6865  sbthlemi10  6979  infmoti  7041  dfmq0qs  7442  dfplq0qs  7443  enq0enq  7444  enq0tr  7447  npsspw  7484  nqprdisj  7557  ltnqpr  7606  ltnqpri  7607  ltexprlemdisj  7619  addcanprg  7629  recexprlemdisj  7643  caucvgprprlemval  7701  addsrpr  7758  mulsrpr  7759  mulgt0sr  7791  addcnsr  7847  mulcnsr  7848  ltresr  7852  addvalex  7857  axcnre  7894  axpre-suploc  7915  supinfneg  9609  infsupneg  9610  xrnemnf  9791  xrnepnf  9792  elfzuzb  10033  fzass4  10076  hashfacen  10830  rexanre  11243  cbvprod  11580  infssuzex  11964  nnwosdc  12054  isprm3  12132  issubm  12885  issubmd  12887  0subm  12897  insubm  12898  isnsg2  13103  lss1d  13629  tgval2  13904  epttop  13943  cnnei  14085  txuni2  14109  txbas  14111  txdis1cn  14131  xmeterval  14288  dedekindicc  14464  lgslem3  14756  bj-stan  14852  nnti  15098