Theorem anbi12i 455

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  anbi12ci  456  ordir  806  orddi  809  dcan  918  3anbi123i  1170  an6  1299  xorcom  1366  trubifal  1394  truxortru  1397  truxorfal  1398  falxortru  1399  falxorfal  1400  nford  1546  nfand  1547  sbequ8  1819  sbanv  1861  sban  1928  sbbi  1932  sbnf2  1956  eu1  2024  2exeu  2091  2eu4  2092  sbabel  2307  neanior  2395  rexeqbii  2448  r19.26m  2563  reean  2599  reu5  2643  reu2  2872  reu3  2874  eqss  3112  unss  3250  ralunb  3257  ssin  3298  undi  3324  difundi  3328  indifdir  3332  inab  3344  difab  3345  reuss2  3356  reupick  3360  raaan  3469  prss  3676  tpss  3685  prsspw  3692  prneimg  3701  uniin  3756  intun  3802  intpr  3803  disjiun  3924  brin  3980  brdif  3981  ssext  4143  pweqb  4145  opthg2  4161  copsex4g  4169  opelopabsb  4182  eqopab2b  4201  pwin  4204  pofun  4234  wetrep  4282  ordwe  4490  wessep  4492  reg3exmidlemwe  4493  elxp3  4593  soinxp  4609  relun  4656  inopab  4671  difopab  4672  inxp  4673  opelco2g  4707  cnvco  4724  dmin  4747  intasym  4923  asymref  4924  cnvdif  4945  xpm  4960  xp11m  4977  dfco2  5038  relssdmrn  5059  cnvpom  5081  xpcom  5085  dffun4  5134  dffun4f  5139  funun  5167  funcnveq  5186  fun11  5190  fununi  5191  imadif  5203  imainlem  5204  imain  5205  fnres  5239  fnopabg  5246  fun  5295  fin  5309  dff1o2  5372  brprcneu  5414  fsn  5592  dff1o6  5677  isotr  5717  brabvv  5817  eqoprab2b  5829  dfoprab3  6089  poxp  6129  cnvoprab  6131  f1od2  6132  brtpos2  6148  tfrlem7  6214  dfer2  6430  eqer  6461  iinerm  6501  brecop  6519  eroveu  6520  erovlem  6521  oviec  6535  mapval2  6572  ixpin  6617  xpcomco  6720  xpassen  6724  ssenen  6745  sbthlemi10  6854  infmoti  6915  dfmq0qs  7237  dfplq0qs  7238  enq0enq  7239  enq0tr  7242  npsspw  7279  nqprdisj  7352  ltnqpr  7401  ltnqpri  7402  ltexprlemdisj  7414  addcanprg  7424  recexprlemdisj  7438  caucvgprprlemval  7496  addsrpr  7553  mulsrpr  7554  mulgt0sr  7586  addcnsr  7642  mulcnsr  7643  ltresr  7647  addvalex  7652  axcnre  7689  axpre-suploc  7710  supinfneg  9390  infsupneg  9391  xrnemnf  9564  xrnepnf  9565  elfzuzb  9800  fzass4  9842  hashfacen  10579  rexanre  10992  cbvprod  11327  infssuzex  11642  isprm3  11799  tgval2  12220  epttop  12259  cnnei  12401  txuni2  12425  txbas  12427  txdis1cn  12447  xmeterval  12604  dedekindicc  12780  bj-stan  12955  nnti  13191