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  817  orddi  820  dcan  933  3anbi123i  1188  an6  1321  xorcom  1388  trubifal  1416  truxortru  1419  truxorfal  1420  falxortru  1421  falxorfal  1422  nford  1567  nfand  1568  sbequ8  1847  sbanv  1889  sban  1955  sbbi  1959  sbnf2  1981  eu1  2051  2exeu  2118  2eu4  2119  sbabel  2346  neanior  2434  rexeqbii  2490  r19.26m  2608  reean  2645  reu5  2689  reu2  2925  reu3  2927  eqss  3170  unss  3309  ralunb  3316  ssin  3357  undi  3383  difundi  3387  indifdir  3391  inab  3403  difab  3404  reuss2  3415  reupick  3419  raaan  3529  prss  3748  tpss  3758  prsspw  3765  prneimg  3774  uniin  3829  intun  3875  intpr  3876  disjiun  3998  brin  4055  brdif  4056  ssext  4221  pweqb  4223  opthg2  4239  copsex4g  4247  opelopabsb  4260  eqopab2b  4279  pwin  4282  pofun  4312  wetrep  4360  ordwe  4575  wessep  4577  reg3exmidlemwe  4578  elxp3  4680  soinxp  4696  relun  4743  inopab  4759  difopab  4760  inxp  4761  opelco2g  4795  cnvco  4812  dmin  4835  restidsing  4963  intasym  5013  asymref  5014  cnvdif  5035  xpm  5050  xp11m  5067  dfco2  5128  relssdmrn  5149  cnvpom  5171  xpcom  5175  dffun4  5227  dffun4f  5232  funun  5260  funcnveq  5279  fun11  5283  fununi  5284  imadif  5296  imainlem  5297  imain  5298  fnres  5332  fnopabg  5339  fun  5388  fin  5402  dff1o2  5466  brprcneu  5508  fsn  5688  dff1o6  5776  isotr  5816  brabvv  5920  eqoprab2b  5932  dfoprab3  6191  poxp  6232  cnvoprab  6234  f1od2  6235  brtpos2  6251  tfrlem7  6317  dfer2  6535  eqer  6566  iinerm  6606  brecop  6624  eroveu  6625  erovlem  6626  oviec  6640  mapval2  6677  ixpin  6722  xpcomco  6825  xpassen  6829  ssenen  6850  sbthlemi10  6964  infmoti  7026  dfmq0qs  7427  dfplq0qs  7428  enq0enq  7429  enq0tr  7432  npsspw  7469  nqprdisj  7542  ltnqpr  7591  ltnqpri  7592  ltexprlemdisj  7604  addcanprg  7614  recexprlemdisj  7628  caucvgprprlemval  7686  addsrpr  7743  mulsrpr  7744  mulgt0sr  7776  addcnsr  7832  mulcnsr  7833  ltresr  7837  addvalex  7842  axcnre  7879  axpre-suploc  7900  supinfneg  9594  infsupneg  9595  xrnemnf  9776  xrnepnf  9777  elfzuzb  10018  fzass4  10061  hashfacen  10815  rexanre  11228  cbvprod  11565  infssuzex  11949  nnwosdc  12039  isprm3  12117  issubm  12862  issubmd  12864  0subm  12870  insubm  12871  isnsg2  13061  tgval2  13521  epttop  13560  cnnei  13702  txuni2  13726  txbas  13728  txdis1cn  13748  xmeterval  13905  dedekindicc  14081  lgslem3  14373  bj-stan  14469  nnti  14714