Theorem anbi12i 460

Description: Conjoin both sides of two equivalences. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
anbi12.1	⊢ (𝜑 ↔ 𝜓)
anbi12.2	⊢ (𝜒 ↔ 𝜃)

Assertion

Ref	Expression
anbi12i	⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))

Proof of Theorem anbi12i

Step	Hyp	Ref	Expression
1		anbi12.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	anbi1i 458	. 2 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒))
3		anbi12.2	. . 3 ⊢ (𝜒 ↔ 𝜃)
4	3	anbi2i 457	. 2 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))
5	2, 4	bitri 184	1 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))

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  1333  xorcom  1407  trubifal  1435  truxortru  1438  truxorfal  1439  falxortru  1440  falxorfal  1441  nford  1589  nfand  1590  sbequ8  1869  sbanv  1912  sban  1982  sbbi  1986  sbnf2  2008  eu1  2078  2exeu  2145  2eu4  2146  sbabel  2374  neanior  2462  rexeqbii  2518  r19.26m  2636  reean  2674  reu5  2722  reu2  2960  reu3  2962  eqss  3207  unss  3346  ralunb  3353  ssin  3394  undi  3420  difundi  3424  indifdir  3428  inab  3440  difab  3441  reuss2  3452  reupick  3456  raaan  3565  prss  3788  tpss  3798  prsspw  3805  prneimg  3814  uniin  3869  intun  3915  intpr  3916  disjiun  4038  brin  4095  brdif  4096  ssext  4264  pweqb  4266  opthg2  4282  copsex4g  4290  opelopabsb  4305  eqopab2b  4325  pwin  4328  pofun  4358  wetrep  4406  ordwe  4623  wessep  4625  reg3exmidlemwe  4626  elxp3  4728  soinxp  4744  relun  4791  inopab  4809  difopab  4810  inxp  4811  opelco2g  4845  cnvco  4862  dmin  4885  restidsing  5014  intasym  5066  asymref  5067  cnvdif  5088  xpm  5103  xp11m  5120  dfco2  5181  relssdmrn  5202  cnvpom  5224  xpcom  5228  dffun4  5281  dffun4f  5286  funun  5314  funcnveq  5336  fun11  5340  fununi  5341  imadif  5353  imainlem  5354  imain  5355  fnres  5391  fnopabg  5398  fun  5447  fin  5461  dff1o2  5526  brprcneu  5568  fsn  5751  dff1o6  5844  isotr  5884  brabvv  5990  eqoprab2b  6002  fvmpopr2d  6081  dfoprab3  6276  poxp  6317  cnvoprab  6319  f1od2  6320  brtpos2  6336  tfrlem7  6402  dfer2  6620  eqer  6651  iinerm  6693  brecop  6711  eroveu  6712  erovlem  6713  oviec  6727  mapval2  6764  ixpin  6809  xpcomco  6920  xpassen  6924  ssenen  6947  sbthlemi10  7067  infmoti  7129  dfmq0qs  7541  dfplq0qs  7542  enq0enq  7543  enq0tr  7546  npsspw  7583  nqprdisj  7656  ltnqpr  7705  ltnqpri  7706  ltexprlemdisj  7718  addcanprg  7728  recexprlemdisj  7742  caucvgprprlemval  7800  addsrpr  7857  mulsrpr  7858  mulgt0sr  7890  addcnsr  7946  mulcnsr  7947  ltresr  7951  addvalex  7956  axcnre  7993  axpre-suploc  8014  supinfneg  9715  infsupneg  9716  xrnemnf  9898  xrnepnf  9899  elfzuzb  10140  fzass4  10183  infssuzex  10374  hashfacen  10979  rexanre  11502  cbvprod  11840  nnwosdc  12331  isprm3  12411  issubm  13275  issubmd  13277  0subm  13287  insubm  13288  isnsg2  13510  lss1d  14116  tgval2  14494  epttop  14533  cnnei  14675  txuni2  14699  txbas  14701  txdis1cn  14721  xmeterval  14878  dedekindicc  15076  plyun0  15179  lgslem3  15450  bj-stan  15645  nnti  15891