Theorem anbi12i 448

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

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  anbi12ci  449  ordir  764  orddi  767  dcan  876  3anbi123i  1128  an6  1253  xorcom  1320  trubifal  1348  truxortru  1351  truxorfal  1352  falxortru  1353  falxorfal  1354  nford  1500  nfand  1501  sbequ8  1770  sbanv  1812  sban  1872  sbbi  1876  sbnf2  1900  eu1  1968  2exeu  2035  2eu4  2036  sbabel  2248  neanior  2336  rexeqbii  2385  r19.26m  2494  reean  2528  reu5  2572  reu2  2791  reu3  2793  eqss  3025  unss  3158  ralunb  3165  ssin  3206  undi  3230  difundi  3234  indifdir  3238  inab  3250  difab  3251  reuss2  3262  reupick  3266  raaan  3369  prss  3567  tpss  3576  prsspw  3583  prneimg  3592  uniin  3647  intun  3693  intpr  3694  brin  3858  brdif  3859  ssext  4012  pweqb  4014  opthg2  4030  copsex4g  4038  opelopabsb  4051  eqopab2b  4070  pwin  4073  pofun  4103  wetrep  4151  ordwe  4354  wessep  4356  reg3exmidlemwe  4357  elxp3  4450  soinxp  4466  relun  4512  inopab  4526  difopab  4527  inxp  4528  opelco2g  4562  cnvco  4579  dmin  4602  intasym  4771  asymref  4772  cnvdif  4792  xpm  4807  xp11m  4823  dfco2  4884  relssdmrn  4905  cnvpom  4927  xpcom  4931  dffun4  4980  dffun4f  4985  funun  5011  funcnveq  5030  fun11  5034  fununi  5035  imadif  5047  imainlem  5048  imain  5049  fnres  5083  fnopabg  5090  fun  5132  fin  5145  dff1o2  5206  brprcneu  5246  fsn  5411  dff1o6  5495  isotr  5535  brabvv  5630  eqoprab2b  5642  dfoprab3  5896  poxp  5932  cnvoprab  5934  f1od2  5935  brtpos2  5948  tfrlem7  6014  dfer2  6223  eqer  6254  iinerm  6294  brecop  6312  eroveu  6313  erovlem  6314  oviec  6328  mapval2  6365  xpcomco  6472  xpassen  6476  ssenen  6497  infmoti  6630  dfmq0qs  6891  dfplq0qs  6892  enq0enq  6893  enq0tr  6896  npsspw  6933  nqprdisj  7006  ltnqpr  7055  ltnqpri  7056  ltexprlemdisj  7068  addcanprg  7078  recexprlemdisj  7092  caucvgprprlemval  7150  addsrpr  7194  mulsrpr  7195  mulgt0sr  7226  addcnsr  7274  mulcnsr  7275  ltresr  7279  addvalex  7284  axcnre  7319  supinfneg  8978  infsupneg  8979  xrnemnf  9143  xrnepnf  9144  elfzuzb  9329  fzass4  9370  hashfacen  10075  rexanre  10480  infssuzex  10725  isprm3  10880  nnti  11234