Theorem anbi12i 433

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

Syntax hints:   /\ wa 97   <-> wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  anbi12ci  434  ordir  730  orddi  733  dcan  842  3anbi123i  1093  an6  1216  xorcom  1279  trubifal  1307  truxortru  1310  truxorfal  1311  falxortru  1312  falxorfal  1313  nford  1459  nfand  1460  sbequ8  1727  sbanv  1769  sban  1829  sbbi  1833  sbnf2  1857  eu1  1925  2exeu  1992  2eu4  1993  sbabel  2203  neanior  2292  rexeqbii  2337  r19.26m  2444  reean  2478  reu5  2522  reu2  2729  reu3  2731  eqss  2960  unss  3117  ralunb  3124  ssin  3159  undi  3185  difundi  3189  indifdir  3193  inab  3205  difab  3206  reuss2  3217  reupick  3221  raaan  3327  prss  3520  tpss  3529  prsspw  3536  prneimg  3545  uniin  3600  intun  3646  intpr  3647  brin  3811  brdif  3812  ssext  3957  pweqb  3959  opthg2  3976  copsex4g  3984  opelopabsb  3997  eqopab2b  4016  pwin  4019  pofun  4049  wetrep  4097  ordwe  4300  wessep  4302  reg3exmidlemwe  4303  elxp3  4394  soinxp  4410  relun  4454  inopab  4468  difopab  4469  inxp  4470  opelco2g  4503  cnvco  4520  dmin  4543  intasym  4709  asymref  4710  cnvdif  4730  xpm  4745  xp11m  4759  dfco2  4820  relssdmrn  4841  cnvpom  4860  xpcom  4864  dffun4  4913  dffun4f  4918  funun  4944  funcnveq  4962  fun11  4966  fununi  4967  imadif  4979  imainlem  4980  imain  4981  fnres  5015  fnopabg  5022  fun  5063  fin  5076  dff1o2  5131  brprcneu  5171  fsn  5335  dff1o6  5416  isotr  5456  brabvv  5551  eqoprab2b  5563  dfoprab3  5817  poxp  5853  brtpos2  5866  tfrlem7  5933  dfer2  6107  eqer  6138  iinerm  6178  brecop  6196  eroveu  6197  erovlem  6198  oviec  6212  xpcomco  6300  xpassen  6304  dfmq0qs  6527  dfplq0qs  6528  enq0enq  6529  enq0tr  6532  npsspw  6569  nqprdisj  6642  ltnqpr  6691  ltnqpri  6692  ltexprlemdisj  6704  addcanprg  6714  recexprlemdisj  6728  caucvgprprlemval  6786  addsrpr  6830  mulsrpr  6831  mulgt0sr  6862  addcnsr  6910  mulcnsr  6911  ltresr  6915  addvalex  6920  axcnre  6955  xrnemnf  8699  xrnepnf  8700  elfzuzb  8884  fzass4  8925