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  729  orddi  732  dcan  841  3anbi123i  1092  an6  1215  xorcom  1276  trubifal  1304  truxortru  1307  truxorfal  1308  falxortru  1309  falxorfal  1310  nford  1456  nfand  1457  sbequ8  1724  sbanv  1766  sban  1826  sbbi  1830  sbnf2  1854  eu1  1922  2exeu  1989  2eu4  1990  sbabel  2200  neanior  2286  rexeqbii  2331  r19.26m  2438  reean  2472  reu5  2516  reu2  2723  reu3  2725  eqss  2954  unss  3111  ralunb  3118  ssin  3153  undi  3179  difundi  3183  indifdir  3187  inab  3199  difab  3200  reuss2  3211  reupick  3215  raaan  3321  prss  3511  tpss  3520  prsspw  3527  prneimg  3536  uniin  3591  intun  3637  intpr  3638  brin  3802  brdif  3803  ssext  3948  pweqb  3950  opthg2  3967  copsex4g  3975  opelopabsb  3988  eqopab2b  4007  pwin  4010  pofun  4040  elxp3  4337  soinxp  4353  relun  4397  inopab  4411  difopab  4412  inxp  4413  opelco2g  4446  cnvco  4463  dmin  4486  intasym  4652  asymref  4653  cnvdif  4673  xpm  4688  xp11m  4702  dfco2  4763  relssdmrn  4784  cnvpom  4803  xpcom  4807  dffun4  4856  dffun4f  4861  funun  4887  funcnveq  4905  fun11  4909  fununi  4910  imadif  4922  imainlem  4923  imain  4924  fnres  4958  fnopabg  4965  fun  5006  fin  5019  dff1o2  5074  brprcneu  5114  fsn  5278  dff1o6  5359  isotr  5399  brabvv  5493  eqoprab2b  5505  dfoprab3  5759  poxp  5794  brtpos2  5807  tfrlem7  5874  dfer2  6043  eqer  6074  iinerm  6114  brecop  6132  eroveu  6133  erovlem  6134  oviec  6148  xpcomco  6236  xpassen  6240  dfmq0qs  6411  dfplq0qs  6412  enq0enq  6413  enq0tr  6416  npsspw  6453  nqprdisj  6527  ltexprlemdisj  6578  addcanprg  6588  recexprlemdisj  6600  addsrpr  6633  mulsrpr  6634  mulgt0sr  6664  addcnsr  6691  mulcnsr  6692  ltresr  6696  axcnre  6725  xrnemnf  8429  xrnepnf  8430  elfzuzb  8614  fzass4  8655