Theorem anbi12i 456

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 454	. 2 |- ( ( ph /\ ch ) <-> ( ps /\ ch ) )
3		anbi12.2	. . 3 |- ( ch <-> th )
4	3	anbi2i 453	. 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  457  ordir  807  orddi  810  dcan  923  3anbi123i  1178  an6  1311  xorcom  1378  trubifal  1406  truxortru  1409  truxorfal  1410  falxortru  1411  falxorfal  1412  nford  1555  nfand  1556  sbequ8  1835  sbanv  1877  sban  1943  sbbi  1947  sbnf2  1969  eu1  2039  2exeu  2106  2eu4  2107  sbabel  2335  neanior  2423  rexeqbii  2479  r19.26m  2597  reean  2634  reu5  2678  reu2  2914  reu3  2916  eqss  3157  unss  3296  ralunb  3303  ssin  3344  undi  3370  difundi  3374  indifdir  3378  inab  3390  difab  3391  reuss2  3402  reupick  3406  raaan  3515  prss  3729  tpss  3738  prsspw  3745  prneimg  3754  uniin  3809  intun  3855  intpr  3856  disjiun  3977  brin  4034  brdif  4035  ssext  4199  pweqb  4201  opthg2  4217  copsex4g  4225  opelopabsb  4238  eqopab2b  4257  pwin  4260  pofun  4290  wetrep  4338  ordwe  4553  wessep  4555  reg3exmidlemwe  4556  elxp3  4658  soinxp  4674  relun  4721  inopab  4736  difopab  4737  inxp  4738  opelco2g  4772  cnvco  4789  dmin  4812  intasym  4988  asymref  4989  cnvdif  5010  xpm  5025  xp11m  5042  dfco2  5103  relssdmrn  5124  cnvpom  5146  xpcom  5150  dffun4  5199  dffun4f  5204  funun  5232  funcnveq  5251  fun11  5255  fununi  5256  imadif  5268  imainlem  5269  imain  5270  fnres  5304  fnopabg  5311  fun  5360  fin  5374  dff1o2  5437  brprcneu  5479  fsn  5657  dff1o6  5744  isotr  5784  brabvv  5888  eqoprab2b  5900  dfoprab3  6159  poxp  6200  cnvoprab  6202  f1od2  6203  brtpos2  6219  tfrlem7  6285  dfer2  6502  eqer  6533  iinerm  6573  brecop  6591  eroveu  6592  erovlem  6593  oviec  6607  mapval2  6644  ixpin  6689  xpcomco  6792  xpassen  6796  ssenen  6817  sbthlemi10  6931  infmoti  6993  dfmq0qs  7370  dfplq0qs  7371  enq0enq  7372  enq0tr  7375  npsspw  7412  nqprdisj  7485  ltnqpr  7534  ltnqpri  7535  ltexprlemdisj  7547  addcanprg  7557  recexprlemdisj  7571  caucvgprprlemval  7629  addsrpr  7686  mulsrpr  7687  mulgt0sr  7719  addcnsr  7775  mulcnsr  7776  ltresr  7780  addvalex  7785  axcnre  7822  axpre-suploc  7843  supinfneg  9533  infsupneg  9534  xrnemnf  9713  xrnepnf  9714  elfzuzb  9954  fzass4  9997  hashfacen  10749  rexanre  11162  cbvprod  11499  infssuzex  11882  nnwosdc  11972  isprm3  12050  tgval2  12691  epttop  12730  cnnei  12872  txuni2  12896  txbas  12898  txdis1cn  12918  xmeterval  13075  dedekindicc  13251  lgslem3  13543  bj-stan  13628  nnti  13874