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  824  orddi  827  3anbi123i  1214  an6  1357  xorcom  1432  trubifal  1460  truxortru  1463  truxorfal  1464  falxortru  1465  falxorfal  1466  nford  1615  nfand  1616  sbequ8  1895  sbanv  1938  sban  2008  sbbi  2012  sbnf2  2034  eu1  2104  2exeu  2172  2eu4  2173  sbabel  2401  neanior  2489  rexeqbii  2545  r19.26m  2664  reean  2702  reu5  2751  cbvreuw  2762  reu2  2994  reu3  2996  eqss  3242  unss  3381  ralunb  3388  ssin  3429  undi  3455  difundi  3459  indifdir  3463  inab  3475  difab  3476  reuss2  3487  reupick  3491  raaan  3600  prss  3829  tpss  3841  prsspw  3848  prneimg  3857  uniin  3913  intun  3959  intpr  3960  disjiun  4083  brin  4141  brdif  4142  ssext  4313  pweqb  4315  opthg2  4331  copsex4g  4339  opelopabsb  4354  eqopab2b  4374  pwin  4379  pofun  4409  wetrep  4457  ordwe  4674  wessep  4676  reg3exmidlemwe  4677  elxp3  4780  soinxp  4796  relun  4844  inopab  4862  difopab  4863  inxp  4864  opelco2g  4898  cnvco  4915  dmin  4939  restidsing  5069  intasym  5121  asymref  5122  cnvdif  5143  xpm  5158  xp11m  5175  dfco2  5236  relssdmrn  5257  cnvpom  5279  xpcom  5283  dffun4  5337  dffun4f  5342  funun  5371  funcnveq  5393  fun11  5397  fununi  5398  imadif  5410  imainlem  5411  imain  5412  fnres  5449  fnopabg  5456  fun  5508  fin  5523  dff1o2  5588  brprcneu  5632  fsn  5819  dff1o6  5916  isotr  5956  brabvv  6066  eqoprab2b  6078  fvmpopr2d  6157  dfoprab3  6353  poxp  6396  cnvoprab  6398  f1od2  6399  brtpos2  6416  tfrlem7  6482  dfer2  6702  eqer  6733  iinerm  6775  brecop  6793  eroveu  6794  erovlem  6795  oviec  6809  mapval2  6846  ixpin  6891  modom  6993  xpcomco  7009  xpassen  7013  ssenen  7036  sbthlemi10  7164  infmoti  7226  dfmq0qs  7648  dfplq0qs  7649  enq0enq  7650  enq0tr  7653  npsspw  7690  nqprdisj  7763  ltnqpr  7812  ltnqpri  7813  ltexprlemdisj  7825  addcanprg  7835  recexprlemdisj  7849  caucvgprprlemval  7907  addsrpr  7964  mulsrpr  7965  mulgt0sr  7997  addcnsr  8053  mulcnsr  8054  ltresr  8058  addvalex  8063  axcnre  8100  axpre-suploc  8121  supinfneg  9828  infsupneg  9829  xrnemnf  10011  xrnepnf  10012  elfzuzb  10253  fzass4  10296  infssuzex  10492  hashfacen  11099  rexanre  11780  cbvprod  12118  nnwosdc  12609  isprm3  12689  issubm  13554  issubmd  13556  0subm  13566  insubm  13567  isnsg2  13789  lss1d  14396  tgval2  14774  epttop  14813  cnnei  14955  txuni2  14979  txbas  14981  txdis1cn  15001  xmeterval  15158  dedekindicc  15356  plyun0  15459  lgslem3  15730  vtxd0nedgbfi  16149  wlk1walkdom  16209  clwwlknonccat  16283  clwwlknon2x  16285  bj-stan  16343  nnti  16591