Theorem anbi12i 457

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 455	. 2 |- ( ( ph /\ ch ) <-> ( ps /\ ch ) )
3		anbi12.2	. . 3 |- ( ch <-> th )
4	3	anbi2i 454	. 2 |- ( ( ps /\ ch ) <-> ( ps /\ th ) )
5	2, 4	bitri 183	1 |- ( ( ph /\ ch ) <-> ( ps /\ th ) )

Syntax hints:   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  anbi12ci  458  ordir  812  orddi  815  dcan  928  3anbi123i  1183  an6  1316  xorcom  1383  trubifal  1411  truxortru  1414  truxorfal  1415  falxortru  1416  falxorfal  1417  nford  1560  nfand  1561  sbequ8  1840  sbanv  1882  sban  1948  sbbi  1952  sbnf2  1974  eu1  2044  2exeu  2111  2eu4  2112  sbabel  2339  neanior  2427  rexeqbii  2483  r19.26m  2601  reean  2638  reu5  2682  reu2  2918  reu3  2920  eqss  3162  unss  3301  ralunb  3308  ssin  3349  undi  3375  difundi  3379  indifdir  3383  inab  3395  difab  3396  reuss2  3407  reupick  3411  raaan  3521  prss  3736  tpss  3745  prsspw  3752  prneimg  3761  uniin  3816  intun  3862  intpr  3863  disjiun  3984  brin  4041  brdif  4042  ssext  4206  pweqb  4208  opthg2  4224  copsex4g  4232  opelopabsb  4245  eqopab2b  4264  pwin  4267  pofun  4297  wetrep  4345  ordwe  4560  wessep  4562  reg3exmidlemwe  4563  elxp3  4665  soinxp  4681  relun  4728  inopab  4743  difopab  4744  inxp  4745  opelco2g  4779  cnvco  4796  dmin  4819  intasym  4995  asymref  4996  cnvdif  5017  xpm  5032  xp11m  5049  dfco2  5110  relssdmrn  5131  cnvpom  5153  xpcom  5157  dffun4  5209  dffun4f  5214  funun  5242  funcnveq  5261  fun11  5265  fununi  5266  imadif  5278  imainlem  5279  imain  5280  fnres  5314  fnopabg  5321  fun  5370  fin  5384  dff1o2  5447  brprcneu  5489  fsn  5668  dff1o6  5755  isotr  5795  brabvv  5899  eqoprab2b  5911  dfoprab3  6170  poxp  6211  cnvoprab  6213  f1od2  6214  brtpos2  6230  tfrlem7  6296  dfer2  6514  eqer  6545  iinerm  6585  brecop  6603  eroveu  6604  erovlem  6605  oviec  6619  mapval2  6656  ixpin  6701  xpcomco  6804  xpassen  6808  ssenen  6829  sbthlemi10  6943  infmoti  7005  dfmq0qs  7391  dfplq0qs  7392  enq0enq  7393  enq0tr  7396  npsspw  7433  nqprdisj  7506  ltnqpr  7555  ltnqpri  7556  ltexprlemdisj  7568  addcanprg  7578  recexprlemdisj  7592  caucvgprprlemval  7650  addsrpr  7707  mulsrpr  7708  mulgt0sr  7740  addcnsr  7796  mulcnsr  7797  ltresr  7801  addvalex  7806  axcnre  7843  axpre-suploc  7864  supinfneg  9554  infsupneg  9555  xrnemnf  9734  xrnepnf  9735  elfzuzb  9975  fzass4  10018  hashfacen  10771  rexanre  11184  cbvprod  11521  infssuzex  11904  nnwosdc  11994  isprm3  12072  issubm  12695  issubmd  12696  0subm  12702  insubm  12703  tgval2  12845  epttop  12884  cnnei  13026  txuni2  13050  txbas  13052  txdis1cn  13072  xmeterval  13229  dedekindicc  13405  lgslem3  13697  bj-stan  13782  nnti  14027