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  878  3anbi123i  1130  an6  1255  xorcom  1322  trubifal  1350  truxortru  1353  truxorfal  1354  falxortru  1355  falxorfal  1356  nford  1502  nfand  1503  sbequ8  1772  sbanv  1814  sban  1874  sbbi  1878  sbnf2  1902  eu1  1970  2exeu  2037  2eu4  2038  sbabel  2250  neanior  2338  rexeqbii  2387  r19.26m  2496  reean  2531  reu5  2575  reu2  2794  reu3  2796  eqss  3029  unss  3163  ralunb  3170  ssin  3211  undi  3236  difundi  3240  indifdir  3244  inab  3256  difab  3257  reuss2  3268  reupick  3272  raaan  3375  prss  3578  tpss  3587  prsspw  3594  prneimg  3603  uniin  3658  intun  3704  intpr  3705  brin  3869  brdif  3870  ssext  4024  pweqb  4026  opthg2  4042  copsex4g  4050  opelopabsb  4063  eqopab2b  4082  pwin  4085  pofun  4115  wetrep  4163  ordwe  4366  wessep  4368  reg3exmidlemwe  4369  elxp3  4462  soinxp  4478  relun  4524  inopab  4538  difopab  4539  inxp  4540  opelco2g  4574  cnvco  4591  dmin  4614  intasym  4785  asymref  4786  cnvdif  4806  xpm  4821  xp11m  4837  dfco2  4898  relssdmrn  4919  cnvpom  4941  xpcom  4945  dffun4  4994  dffun4f  4999  funun  5025  funcnveq  5044  fun11  5048  fununi  5049  imadif  5061  imainlem  5062  imain  5063  fnres  5097  fnopabg  5104  fun  5149  fin  5162  dff1o2  5223  brprcneu  5263  fsn  5434  dff1o6  5518  isotr  5558  brabvv  5654  eqoprab2b  5666  dfoprab3  5920  poxp  5956  cnvoprab  5958  f1od2  5959  brtpos2  5972  tfrlem7  6038  dfer2  6247  eqer  6278  iinerm  6318  brecop  6336  eroveu  6337  erovlem  6338  oviec  6352  mapval2  6389  xpcomco  6496  xpassen  6500  ssenen  6521  sbthlemi10  6622  infmoti  6670  dfmq0qs  6935  dfplq0qs  6936  enq0enq  6937  enq0tr  6940  npsspw  6977  nqprdisj  7050  ltnqpr  7099  ltnqpri  7100  ltexprlemdisj  7112  addcanprg  7122  recexprlemdisj  7136  caucvgprprlemval  7194  addsrpr  7238  mulsrpr  7239  mulgt0sr  7270  addcnsr  7318  mulcnsr  7319  ltresr  7323  addvalex  7328  axcnre  7363  supinfneg  9018  infsupneg  9019  xrnemnf  9183  xrnepnf  9184  elfzuzb  9369  fzass4  9410  hashfacen  10159  rexanre  10570  infssuzex  10870  isprm3  11025  nnti  11380