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  2289  rexeqbii  2334  r19.26m  2441  reean  2475  reu5  2519  reu2  2726  reu3  2728  eqss  2957  unss  3114  ralunb  3121  ssin  3156  undi  3182  difundi  3186  indifdir  3190  inab  3202  difab  3203  reuss2  3214  reupick  3218  raaan  3324  prss  3517  tpss  3526  prsspw  3533  prneimg  3542  uniin  3597  intun  3643  intpr  3644  brin  3808  brdif  3809  ssext  3954  pweqb  3956  opthg2  3973  copsex4g  3981  opelopabsb  3994  eqopab2b  4013  pwin  4016  pofun  4046  wetrep  4093  elxp3  4381  soinxp  4397  relun  4441  inopab  4455  difopab  4456  inxp  4457  opelco2g  4490  cnvco  4507  dmin  4530  intasym  4696  asymref  4697  cnvdif  4717  xpm  4732  xp11m  4746  dfco2  4807  relssdmrn  4828  cnvpom  4847  xpcom  4851  dffun4  4900  dffun4f  4905  funun  4931  funcnveq  4949  fun11  4953  fununi  4954  imadif  4966  imainlem  4967  imain  4968  fnres  5002  fnopabg  5009  fun  5050  fin  5063  dff1o2  5118  brprcneu  5158  fsn  5322  dff1o6  5403  isotr  5443  brabvv  5538  eqoprab2b  5550  dfoprab3  5804  poxp  5840  brtpos2  5853  tfrlem7  5920  dfer2  6094  eqer  6125  iinerm  6165  brecop  6183  eroveu  6184  erovlem  6185  oviec  6199  xpcomco  6287  xpassen  6291  dfmq0qs  6508  dfplq0qs  6509  enq0enq  6510  enq0tr  6513  npsspw  6550  nqprdisj  6623  ltnqpr  6672  ltnqpri  6673  ltexprlemdisj  6685  addcanprg  6695  recexprlemdisj  6709  caucvgprprlemval  6767  addsrpr  6811  mulsrpr  6812  mulgt0sr  6843  addcnsr  6891  mulcnsr  6892  ltresr  6896  addvalex  6901  axcnre  6936  xrnemnf  8666  xrnepnf  8667  elfzuzb  8851  fzass4  8892