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  817  orddi  820  dcan  933  3anbi123i  1188  an6  1321  xorcom  1388  trubifal  1416  truxortru  1419  truxorfal  1420  falxortru  1421  falxorfal  1422  nford  1567  nfand  1568  sbequ8  1847  sbanv  1889  sban  1955  sbbi  1959  sbnf2  1981  eu1  2051  2exeu  2118  2eu4  2119  sbabel  2346  neanior  2434  rexeqbii  2490  r19.26m  2608  reean  2646  reu5  2690  reu2  2926  reu3  2928  eqss  3171  unss  3310  ralunb  3317  ssin  3358  undi  3384  difundi  3388  indifdir  3392  inab  3404  difab  3405  reuss2  3416  reupick  3420  raaan  3530  prss  3749  tpss  3759  prsspw  3766  prneimg  3775  uniin  3830  intun  3876  intpr  3877  disjiun  3999  brin  4056  brdif  4057  ssext  4222  pweqb  4224  opthg2  4240  copsex4g  4248  opelopabsb  4261  eqopab2b  4280  pwin  4283  pofun  4313  wetrep  4361  ordwe  4576  wessep  4578  reg3exmidlemwe  4579  elxp3  4681  soinxp  4697  relun  4744  inopab  4760  difopab  4761  inxp  4762  opelco2g  4796  cnvco  4813  dmin  4836  restidsing  4964  intasym  5014  asymref  5015  cnvdif  5036  xpm  5051  xp11m  5068  dfco2  5129  relssdmrn  5150  cnvpom  5172  xpcom  5176  dffun4  5228  dffun4f  5233  funun  5261  funcnveq  5280  fun11  5284  fununi  5285  imadif  5297  imainlem  5298  imain  5299  fnres  5333  fnopabg  5340  fun  5389  fin  5403  dff1o2  5467  brprcneu  5509  fsn  5689  dff1o6  5777  isotr  5817  brabvv  5921  eqoprab2b  5933  dfoprab3  6192  poxp  6233  cnvoprab  6235  f1od2  6236  brtpos2  6252  tfrlem7  6318  dfer2  6536  eqer  6567  iinerm  6607  brecop  6625  eroveu  6626  erovlem  6627  oviec  6641  mapval2  6678  ixpin  6723  xpcomco  6826  xpassen  6830  ssenen  6851  sbthlemi10  6965  infmoti  7027  dfmq0qs  7428  dfplq0qs  7429  enq0enq  7430  enq0tr  7433  npsspw  7470  nqprdisj  7543  ltnqpr  7592  ltnqpri  7593  ltexprlemdisj  7605  addcanprg  7615  recexprlemdisj  7629  caucvgprprlemval  7687  addsrpr  7744  mulsrpr  7745  mulgt0sr  7777  addcnsr  7833  mulcnsr  7834  ltresr  7838  addvalex  7843  axcnre  7880  axpre-suploc  7901  supinfneg  9595  infsupneg  9596  xrnemnf  9777  xrnepnf  9778  elfzuzb  10019  fzass4  10062  hashfacen  10816  rexanre  11229  cbvprod  11566  infssuzex  11950  nnwosdc  12040  isprm3  12118  issubm  12863  issubmd  12865  0subm  12871  insubm  12872  isnsg2  13063  tgval2  13554  epttop  13593  cnnei  13735  txuni2  13759  txbas  13761  txdis1cn  13781  xmeterval  13938  dedekindicc  14114  lgslem3  14406  bj-stan  14502  nnti  14747