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  819  orddi  822  3anbi123i  1191  an6  1334  xorcom  1408  trubifal  1436  truxortru  1439  truxorfal  1440  falxortru  1441  falxorfal  1442  nford  1590  nfand  1591  sbequ8  1870  sbanv  1913  sban  1983  sbbi  1987  sbnf2  2009  eu1  2079  2exeu  2146  2eu4  2147  sbabel  2375  neanior  2463  rexeqbii  2519  r19.26m  2637  reean  2675  reu5  2723  reu2  2961  reu3  2963  eqss  3208  unss  3347  ralunb  3354  ssin  3395  undi  3421  difundi  3425  indifdir  3429  inab  3441  difab  3442  reuss2  3453  reupick  3457  raaan  3566  prss  3789  tpss  3799  prsspw  3806  prneimg  3815  uniin  3870  intun  3916  intpr  3917  disjiun  4040  brin  4097  brdif  4098  ssext  4266  pweqb  4268  opthg2  4284  copsex4g  4292  opelopabsb  4307  eqopab2b  4327  pwin  4330  pofun  4360  wetrep  4408  ordwe  4625  wessep  4627  reg3exmidlemwe  4628  elxp3  4730  soinxp  4746  relun  4793  inopab  4811  difopab  4812  inxp  4813  opelco2g  4847  cnvco  4864  dmin  4887  restidsing  5016  intasym  5068  asymref  5069  cnvdif  5090  xpm  5105  xp11m  5122  dfco2  5183  relssdmrn  5204  cnvpom  5226  xpcom  5230  dffun4  5283  dffun4f  5288  funun  5316  funcnveq  5338  fun11  5342  fununi  5343  imadif  5355  imainlem  5356  imain  5357  fnres  5394  fnopabg  5401  fun  5450  fin  5464  dff1o2  5529  brprcneu  5571  fsn  5754  dff1o6  5847  isotr  5887  brabvv  5993  eqoprab2b  6005  fvmpopr2d  6084  dfoprab3  6279  poxp  6320  cnvoprab  6322  f1od2  6323  brtpos2  6339  tfrlem7  6405  dfer2  6623  eqer  6654  iinerm  6696  brecop  6714  eroveu  6715  erovlem  6716  oviec  6730  mapval2  6767  ixpin  6812  xpcomco  6923  xpassen  6927  ssenen  6950  sbthlemi10  7070  infmoti  7132  dfmq0qs  7544  dfplq0qs  7545  enq0enq  7546  enq0tr  7549  npsspw  7586  nqprdisj  7659  ltnqpr  7708  ltnqpri  7709  ltexprlemdisj  7721  addcanprg  7731  recexprlemdisj  7745  caucvgprprlemval  7803  addsrpr  7860  mulsrpr  7861  mulgt0sr  7893  addcnsr  7949  mulcnsr  7950  ltresr  7954  addvalex  7959  axcnre  7996  axpre-suploc  8017  supinfneg  9718  infsupneg  9719  xrnemnf  9901  xrnepnf  9902  elfzuzb  10143  fzass4  10186  infssuzex  10378  hashfacen  10983  rexanre  11564  cbvprod  11902  nnwosdc  12393  isprm3  12473  issubm  13337  issubmd  13339  0subm  13349  insubm  13350  isnsg2  13572  lss1d  14178  tgval2  14556  epttop  14595  cnnei  14737  txuni2  14761  txbas  14763  txdis1cn  14783  xmeterval  14940  dedekindicc  15138  plyun0  15241  lgslem3  15512  bj-stan  15720  nnti  15966