Theorem anbi12i 678

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

Syntax hints:   <-> wb 176   /\ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  anbi12ci  679  ordi  834  ordir  835  orddi  839  pm5.17  858  xor  861  3anbi123i  1140  an6  1261  nanbi  1294  cadan  1392  nic-axALT  1439  19.43OLD  1606  nfimdOLD  1809  sbbi  2071  sbnf2  2108  eu1  2225  2eu1  2284  2eu4  2287  2eu6  2289  sbabel  2516  neanior  2602  rexeqbii  2646  r19.26m  2750  reean  2778  2ralor  2781  reu5  2825  reu2  3025  reu3  3027  2reu5lem3  3044  eqss  3288  unss  3438  ralunb  3445  ssin  3478  undi  3503  indifdir  3512  undif3  3516  inab  3523  difab  3524  reuss2  3536  reupick  3540  prss  3862  sstp  3871  tpss  3872  prsspw  3879  uniin  3912  intun  3959  intpr  3960  inxpk  4278  sikexlem  4296  dfidk2  4314  ndisjrelk  4324  dfpw2  4328  dfaddc2  4382  dfnnc2  4396  addccom  4407  addcass  4416  nnsucelrlem1  4425  nnsucelrlem2  4426  preaddccan2lem1  4455  ltfinex  4465  ssfin  4471  eqpw1relk  4480  ncfinraiselem2  4481  ncfinraise  4482  ncfinlowerlem1  4483  ncfinlower  4484  eqtfinrelk  4487  evenfinex  4504  oddfinex  4505  evenodddisjlem1  4516  nnadjoinlem1  4520  nnpweqlem1  4523  nnpweq  4524  srelk  4525  sfin112  4530  sfintfinlem1  4532  tfinnnlem1  4534  sfinltfin  4536  spfinex  4538  dfphi2  4570  dfop2lem1  4574  copsex4g  4611  opeqexb  4621  brin  4694  brdif  4695  setconslem1  4732  setconslem2  4733  dfswap2  4742  dfco1  4749  opelxp  4812  elxp3  4832  opbrop  4842  eqrel  4846  eqopr  4848  inopab  4863  inxp  4864  cnvco  4895  dmin  4914  cnvdif  5035  xpnz  5046  xp11  5057  dfco2  5081  dfxp2  5114  dffun4  5122  funun  5147  fun11  5160  fununi  5161  imadif  5172  fnres  5200  fnopabg  5206  fco  5232  fun  5237  fin  5247  f1co  5265  foco  5280  dff1o2  5292  f1oco  5309  tz6.12  5346  fsn  5433  dff1o6  5476  isotr  5496  isomin  5497  dfid4  5504  1stfo  5506  2ndfo  5507  funsi  5521  trtxp  5782  oteltxp  5783  brtxp  5784  dmtxp  5803  txpcofun  5804  fntxp  5805  otsnelsi3  5806  releqmpt  5809  releqmpt2  5810  composeex  5821  disjex  5824  addcfnex  5825  funsex  5829  fnsex  5833  qrpprod  5837  dmpprod  5841  fnpprod  5844  f1opprod  5845  crossex  5851  pw1fnex  5853  pw1fnf1o  5856  fnfullfunlem1  5857  domfnex  5871  ranfnex  5872  clos1ex  5877  dfnnc3  5886  transex  5911  refex  5912  antisymex  5913  connexex  5914  foundex  5915  extex  5916  symex  5917  ider  5944  ssetpov  5945  eqer  5962  mapexi  6004  mapval2  6019  enex  6032  entr  6039  fundmen  6044  unen  6049  xpen  6056  xpassenlem  6057  xpassen  6058  enpw1lem1  6062  enpw1  6063  enmap2lem4  6067  enmap1lem4  6073  enprmaplem1  6077  enprmaplem4  6080  nenpw1pwlem1  6085  lecex  6116  ovmuc  6131  mucnc  6132  muccl  6133  mucex  6134  muccom  6135  ncdisjeq  6149  tcdi  6165  ovcelem1  6172  ceexlem1  6174  ceex  6175  ce0addcnnul  6180  sbthlem3  6206  sbth  6207  dflec3  6222  nclenc  6223  lenc  6224  tc11  6229  ce2le  6234  tcfnex  6245  muc0or  6253  nnltp1clem1  6262  addccan2nclem2  6265  nmembers1lem1  6269  nncdiv3lem1  6276  nncdiv3lem2  6277  nnc3n3p1  6279  spacvallem1  6282  nchoicelem10  6299  nchoicelem11  6300  nchoicelem16  6305  fnfreclem1  6318