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  1895  sbanv  1938  sban  2008  sbbi  2012  sbnf2  2034  eu1  2104  2exeu  2172  2eu4  2173  sbabel  2401  neanior  2489  rexeqbii  2545  r19.26m  2664  reean  2702  reu5  2751  cbvreuw  2762  reu2  2994  reu3  2996  eqss  3242  unss  3381  ralunb  3388  ssin  3429  undi  3455  difundi  3459  indifdir  3463  inab  3475  difab  3476  reuss2  3487  reupick  3491  raaan  3600  prss  3829  tpss  3841  prsspw  3848  prneimg  3857  uniin  3913  intun  3959  intpr  3960  disjiun  4083  brin  4141  brdif  4142  ssext  4313  pweqb  4315  opthg2  4331  copsex4g  4339  opelopabsb  4354  eqopab2b  4374  pwin  4379  pofun  4409  wetrep  4457  ordwe  4674  wessep  4676  reg3exmidlemwe  4677  elxp3  4780  soinxp  4796  relun  4844  inopab  4862  difopab  4863  inxp  4864  opelco2g  4898  cnvco  4915  dmin  4939  restidsing  5069  intasym  5121  asymref  5122  cnvdif  5143  xpm  5158  xp11m  5175  dfco2  5236  relssdmrn  5257  cnvpom  5279  xpcom  5283  dffun4  5337  dffun4f  5342  funun  5371  funcnveq  5393  fun11  5397  fununi  5398  imadif  5410  imainlem  5411  imain  5412  fnres  5449  fnopabg  5456  fun  5508  fin  5523  dff1o2  5589  brprcneu  5633  fsn  5820  dff1o6  5920  isotr  5960  brabvv  6070  eqoprab2b  6082  fvmpopr2d  6161  dfoprab3  6357  poxp  6400  cnvoprab  6402  f1od2  6403  brtpos2  6420  tfrlem7  6486  dfer2  6706  eqer  6737  iinerm  6779  brecop  6797  eroveu  6798  erovlem  6799  oviec  6813  mapval2  6850  ixpin  6895  modom  6997  xpcomco  7013  xpassen  7017  ssenen  7040  sbthlemi10  7168  infmoti  7230  dfmq0qs  7652  dfplq0qs  7653  enq0enq  7654  enq0tr  7657  npsspw  7694  nqprdisj  7767  ltnqpr  7816  ltnqpri  7817  ltexprlemdisj  7829  addcanprg  7839  recexprlemdisj  7853  caucvgprprlemval  7911  addsrpr  7968  mulsrpr  7969  mulgt0sr  8001  addcnsr  8057  mulcnsr  8058  ltresr  8062  addvalex  8067  axcnre  8104  axpre-suploc  8125  supinfneg  9832  infsupneg  9833  xrnemnf  10015  xrnepnf  10016  elfzuzb  10257  fzass4  10300  infssuzex  10497  hashfacen  11104  rexanre  11801  cbvprod  12140  nnwosdc  12631  isprm3  12711  issubm  13576  issubmd  13578  0subm  13588  insubm  13589  isnsg2  13811  lss1d  14419  tgval2  14802  epttop  14841  cnnei  14983  txuni2  15007  txbas  15009  txdis1cn  15029  xmeterval  15186  dedekindicc  15384  plyun0  15487  lgslem3  15758  vtxd0nedgbfi  16177  wlk1walkdom  16237  clwwlknonccat  16311  clwwlknon2x  16313  bj-stan  16402  nnti  16650