Theorem anbi12i 464

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

Syntax hints:   /\ wa 104   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  anbi12ci  465  ordir  829  orddi  832  3anbi123i  1219  an6  1362  xorcom  1437  trubifal  1465  truxortru  1468  truxorfal  1469  falxortru  1470  falxorfal  1471  nford  1620  nfand  1621  sbequ8  1900  sbanv  1944  sban  2015  sbbi  2019  sbnf2  2041  eu1  2111  2exeu  2179  2eu4  2180  sbabel  2419  neanior  2507  rexeqbii  2563  r19.26m  2682  reean  2720  reu5  2770  cbvreuw  2781  reu2  3014  reu3  3016  eqss  3263  unss  3403  ralunb  3410  ssin  3453  undi  3479  difundi  3483  indifdir  3487  inab  3499  difab  3500  reuss2  3513  reupick  3517  raaan  3633  prss  3869  tpss  3881  prsspw  3888  prneimg  3897  uniin  3953  intun  3999  intpr  4000  disjiun  4123  brin  4181  brdif  4182  ssext  4359  pweqb  4361  opthg2  4377  copsex4g  4385  opelopabsb  4400  eqopab2b  4420  pwin  4425  pofun  4455  wetrep  4503  ordwe  4721  wessep  4723  reg3exmidlemwe  4724  elxp3  4827  soinxp  4843  relun  4892  inopab  4910  difopab  4911  inxp  4912  opelco2g  4946  cnvco  4963  dmin  4987  restidsing  5117  intasym  5170  asymref  5171  cnvdif  5192  xpm  5207  xp11m  5224  dfco2  5285  relssdmrn  5306  cnvpom  5328  xpcom  5332  dffun4  5386  dffun4f  5391  funun  5420  funcnveq  5442  fun11  5446  fununi  5447  imadif  5459  imainlem  5460  imain  5461  fnres  5498  fnopabg  5505  fun  5559  fin  5576  dff1o2  5642  brprcneu  5686  fsn  5874  dff1o6  5975  isotr  6015  brabvv  6127  eqoprab2b  6139  fvmpopr2d  6218  dfoprab3  6418  poxp  6461  cnvoprab  6463  f1od2  6464  brtpos2  6515  tfrlem7  6581  dfer2  6801  eqer  6832  iinerm  6874  brecop  6892  eroveu  6893  erovlem  6894  oviec  6908  mapval2  6952  ixpin  6998  modom  7101  xpcomco  7117  xpassen  7121  ssenen  7145  sbthlemi10  7276  infmoti  7361  dfmq0qs  7789  dfplq0qs  7790  enq0enq  7791  enq0tr  7794  npsspw  7831  nqprdisj  7904  ltnqpr  7953  ltnqpri  7954  ltexprlemdisj  7966  addcanprg  7976  recexprlemdisj  7990  caucvgprprlemval  8048  addsrpr  8105  mulsrpr  8106  mulgt0sr  8138  addcnsr  8194  mulcnsr  8195  ltresr  8199  addvalex  8204  axcnre  8241  axpre-suploc  8262  supinfneg  9977  infsupneg  9978  xrnemnf  10161  xrnepnf  10162  elfzuzb  10404  fzass4  10449  infssuzex  10647  hashfibclem  11263  hashfacen  11265  rexanre  11967  cbvprod  12306  nnwosdc  12797  isprm3  12877  issubm  13759  issubmd  13761  0subm  13771  insubm  13772  isnsg2  13986  lss1d  14695  tgval2  15078  epttop  15117  cnnei  15259  txuni2  15283  txbas  15285  txdis1cn  15305  xmeterval  15462  dedekindicc  15660  plyun0  15763  lgslem3  16038  vtxd0nedgbfi  16457  wlk1walkdom  16517  clwwlknonccat  16591  clwwlknon2x  16593  bj-stan  16692  nnti  16939  dfrals2  17038  alsbii  17049  ralsbii  17050  cbvals  17054  rals-no-surprise  17056