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  825  orddi  828  3anbi123i  1215  an6  1358  xorcom  1433  trubifal  1461  truxortru  1464  truxorfal  1465  falxortru  1466  falxorfal  1467  nford  1616  nfand  1617  sbequ8  1895  sbanv  1938  sban  2008  sbbi  2012  sbnf2  2034  eu1  2104  2exeu  2172  2eu4  2173  sbabel  2402  neanior  2490  rexeqbii  2546  r19.26m  2665  reean  2703  reu5  2752  cbvreuw  2763  reu2  2995  reu3  2997  eqss  3243  unss  3383  ralunb  3390  ssin  3431  undi  3457  difundi  3461  indifdir  3465  inab  3477  difab  3478  reuss2  3489  reupick  3493  raaan  3602  prss  3834  tpss  3846  prsspw  3853  prneimg  3862  uniin  3918  intun  3964  intpr  3965  disjiun  4088  brin  4146  brdif  4147  ssext  4319  pweqb  4321  opthg2  4337  copsex4g  4345  opelopabsb  4360  eqopab2b  4380  pwin  4385  pofun  4415  wetrep  4463  ordwe  4680  wessep  4682  reg3exmidlemwe  4683  elxp3  4786  soinxp  4802  relun  4850  inopab  4868  difopab  4869  inxp  4870  opelco2g  4904  cnvco  4921  dmin  4945  restidsing  5075  intasym  5128  asymref  5129  cnvdif  5150  xpm  5165  xp11m  5182  dfco2  5243  relssdmrn  5264  cnvpom  5286  xpcom  5290  dffun4  5344  dffun4f  5349  funun  5378  funcnveq  5400  fun11  5404  fununi  5405  imadif  5417  imainlem  5418  imain  5419  fnres  5456  fnopabg  5463  fun  5516  fin  5531  dff1o2  5597  brprcneu  5641  fsn  5827  dff1o6  5927  isotr  5967  brabvv  6077  eqoprab2b  6089  fvmpopr2d  6168  dfoprab3  6363  poxp  6406  cnvoprab  6408  f1od2  6409  brtpos2  6460  tfrlem7  6526  dfer2  6746  eqer  6777  iinerm  6819  brecop  6837  eroveu  6838  erovlem  6839  oviec  6853  mapval2  6890  ixpin  6935  modom  7037  xpcomco  7053  xpassen  7057  ssenen  7080  sbthlemi10  7208  infmoti  7270  dfmq0qs  7692  dfplq0qs  7693  enq0enq  7694  enq0tr  7697  npsspw  7734  nqprdisj  7807  ltnqpr  7856  ltnqpri  7857  ltexprlemdisj  7869  addcanprg  7879  recexprlemdisj  7893  caucvgprprlemval  7951  addsrpr  8008  mulsrpr  8009  mulgt0sr  8041  addcnsr  8097  mulcnsr  8098  ltresr  8102  addvalex  8107  axcnre  8144  axpre-suploc  8165  supinfneg  9873  infsupneg  9874  xrnemnf  10056  xrnepnf  10057  elfzuzb  10299  fzass4  10342  infssuzex  10539  hashfacen  11146  rexanre  11843  cbvprod  12182  nnwosdc  12673  isprm3  12753  issubm  13618  issubmd  13620  0subm  13630  insubm  13631  isnsg2  13853  lss1d  14462  tgval2  14845  epttop  14884  cnnei  15026  txuni2  15050  txbas  15052  txdis1cn  15072  xmeterval  15229  dedekindicc  15427  plyun0  15530  lgslem3  15804  vtxd0nedgbfi  16223  wlk1walkdom  16283  clwwlknonccat  16357  clwwlknon2x  16359  bj-stan  16448  nnti  16695