Theorem anbi12i 460

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 458	. 2 |- ( ( ph /\ ch ) <-> ( ps /\ ch ) )
3		anbi12.2	. . 3 |- ( ch <-> th )
4	3	anbi2i 457	. 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  461  ordir  818  orddi  821  3anbi123i  1190  an6  1332  xorcom  1399  trubifal  1427  truxortru  1430  truxorfal  1431  falxortru  1432  falxorfal  1433  nford  1578  nfand  1579  sbequ8  1858  sbanv  1901  sban  1971  sbbi  1975  sbnf2  1997  eu1  2067  2exeu  2134  2eu4  2135  sbabel  2363  neanior  2451  rexeqbii  2507  r19.26m  2625  reean  2663  reu5  2711  reu2  2948  reu3  2950  eqss  3194  unss  3333  ralunb  3340  ssin  3381  undi  3407  difundi  3411  indifdir  3415  inab  3427  difab  3428  reuss2  3439  reupick  3443  raaan  3552  prss  3774  tpss  3784  prsspw  3791  prneimg  3800  uniin  3855  intun  3901  intpr  3902  disjiun  4024  brin  4081  brdif  4082  ssext  4250  pweqb  4252  opthg2  4268  copsex4g  4276  opelopabsb  4290  eqopab2b  4310  pwin  4313  pofun  4343  wetrep  4391  ordwe  4608  wessep  4610  reg3exmidlemwe  4611  elxp3  4713  soinxp  4729  relun  4776  inopab  4794  difopab  4795  inxp  4796  opelco2g  4830  cnvco  4847  dmin  4870  restidsing  4998  intasym  5050  asymref  5051  cnvdif  5072  xpm  5087  xp11m  5104  dfco2  5165  relssdmrn  5186  cnvpom  5208  xpcom  5212  dffun4  5265  dffun4f  5270  funun  5298  funcnveq  5317  fun11  5321  fununi  5322  imadif  5334  imainlem  5335  imain  5336  fnres  5370  fnopabg  5377  fun  5426  fin  5440  dff1o2  5505  brprcneu  5547  fsn  5730  dff1o6  5819  isotr  5859  brabvv  5964  eqoprab2b  5976  dfoprab3  6244  poxp  6285  cnvoprab  6287  f1od2  6288  brtpos2  6304  tfrlem7  6370  dfer2  6588  eqer  6619  iinerm  6661  brecop  6679  eroveu  6680  erovlem  6681  oviec  6695  mapval2  6732  ixpin  6777  xpcomco  6880  xpassen  6884  ssenen  6907  sbthlemi10  7025  infmoti  7087  dfmq0qs  7489  dfplq0qs  7490  enq0enq  7491  enq0tr  7494  npsspw  7531  nqprdisj  7604  ltnqpr  7653  ltnqpri  7654  ltexprlemdisj  7666  addcanprg  7676  recexprlemdisj  7690  caucvgprprlemval  7748  addsrpr  7805  mulsrpr  7806  mulgt0sr  7838  addcnsr  7894  mulcnsr  7895  ltresr  7899  addvalex  7904  axcnre  7941  axpre-suploc  7962  supinfneg  9660  infsupneg  9661  xrnemnf  9843  xrnepnf  9844  elfzuzb  10085  fzass4  10128  hashfacen  10907  rexanre  11364  cbvprod  11701  infssuzex  12086  nnwosdc  12176  isprm3  12256  issubm  13044  issubmd  13046  0subm  13056  insubm  13057  isnsg2  13273  lss1d  13879  tgval2  14219  epttop  14258  cnnei  14400  txuni2  14424  txbas  14426  txdis1cn  14446  xmeterval  14603  dedekindicc  14787  plyun0  14882  lgslem3  15118  bj-stan  15239  nnti  15485