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  5588  brprcneu  5632  fsn  5819  dff1o6  5917  isotr  5957  brabvv  6067  eqoprab2b  6079  fvmpopr2d  6158  dfoprab3  6354  poxp  6397  cnvoprab  6399  f1od2  6400  brtpos2  6417  tfrlem7  6483  dfer2  6703  eqer  6734  iinerm  6776  brecop  6794  eroveu  6795  erovlem  6796  oviec  6810  mapval2  6847  ixpin  6892  modom  6994  xpcomco  7010  xpassen  7014  ssenen  7037  sbthlemi10  7165  infmoti  7227  dfmq0qs  7649  dfplq0qs  7650  enq0enq  7651  enq0tr  7654  npsspw  7691  nqprdisj  7764  ltnqpr  7813  ltnqpri  7814  ltexprlemdisj  7826  addcanprg  7836  recexprlemdisj  7850  caucvgprprlemval  7908  addsrpr  7965  mulsrpr  7966  mulgt0sr  7998  addcnsr  8054  mulcnsr  8055  ltresr  8059  addvalex  8064  axcnre  8101  axpre-suploc  8122  supinfneg  9829  infsupneg  9830  xrnemnf  10012  xrnepnf  10013  elfzuzb  10254  fzass4  10297  infssuzex  10493  hashfacen  11100  rexanre  11781  cbvprod  12120  nnwosdc  12611  isprm3  12691  issubm  13556  issubmd  13558  0subm  13568  insubm  13569  isnsg2  13791  lss1d  14399  tgval2  14777  epttop  14816  cnnei  14958  txuni2  14982  txbas  14984  txdis1cn  15004  xmeterval  15161  dedekindicc  15359  plyun0  15462  lgslem3  15733  vtxd0nedgbfi  16152  wlk1walkdom  16212  clwwlknonccat  16286  clwwlknon2x  16288  bj-stan  16346  nnti  16594