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  819  orddi  822  3anbi123i  1191  an6  1334  xorcom  1408  trubifal  1436  truxortru  1439  truxorfal  1440  falxortru  1441  falxorfal  1442  nford  1590  nfand  1591  sbequ8  1870  sbanv  1913  sban  1983  sbbi  1987  sbnf2  2009  eu1  2079  2exeu  2146  2eu4  2147  sbabel  2375  neanior  2463  rexeqbii  2519  r19.26m  2637  reean  2675  reu5  2723  reu2  2961  reu3  2963  eqss  3208  unss  3347  ralunb  3354  ssin  3395  undi  3421  difundi  3425  indifdir  3429  inab  3441  difab  3442  reuss2  3453  reupick  3457  raaan  3566  prss  3789  tpss  3799  prsspw  3806  prneimg  3815  uniin  3870  intun  3916  intpr  3917  disjiun  4039  brin  4096  brdif  4097  ssext  4265  pweqb  4267  opthg2  4283  copsex4g  4291  opelopabsb  4306  eqopab2b  4326  pwin  4329  pofun  4359  wetrep  4407  ordwe  4624  wessep  4626  reg3exmidlemwe  4627  elxp3  4729  soinxp  4745  relun  4792  inopab  4810  difopab  4811  inxp  4812  opelco2g  4846  cnvco  4863  dmin  4886  restidsing  5015  intasym  5067  asymref  5068  cnvdif  5089  xpm  5104  xp11m  5121  dfco2  5182  relssdmrn  5203  cnvpom  5225  xpcom  5229  dffun4  5282  dffun4f  5287  funun  5315  funcnveq  5337  fun11  5341  fununi  5342  imadif  5354  imainlem  5355  imain  5356  fnres  5392  fnopabg  5399  fun  5448  fin  5462  dff1o2  5527  brprcneu  5569  fsn  5752  dff1o6  5845  isotr  5885  brabvv  5991  eqoprab2b  6003  fvmpopr2d  6082  dfoprab3  6277  poxp  6318  cnvoprab  6320  f1od2  6321  brtpos2  6337  tfrlem7  6403  dfer2  6621  eqer  6652  iinerm  6694  brecop  6712  eroveu  6713  erovlem  6714  oviec  6728  mapval2  6765  ixpin  6810  xpcomco  6921  xpassen  6925  ssenen  6948  sbthlemi10  7068  infmoti  7130  dfmq0qs  7542  dfplq0qs  7543  enq0enq  7544  enq0tr  7547  npsspw  7584  nqprdisj  7657  ltnqpr  7706  ltnqpri  7707  ltexprlemdisj  7719  addcanprg  7729  recexprlemdisj  7743  caucvgprprlemval  7801  addsrpr  7858  mulsrpr  7859  mulgt0sr  7891  addcnsr  7947  mulcnsr  7948  ltresr  7952  addvalex  7957  axcnre  7994  axpre-suploc  8015  supinfneg  9716  infsupneg  9717  xrnemnf  9899  xrnepnf  9900  elfzuzb  10141  fzass4  10184  infssuzex  10376  hashfacen  10981  rexanre  11531  cbvprod  11869  nnwosdc  12360  isprm3  12440  issubm  13304  issubmd  13306  0subm  13316  insubm  13317  isnsg2  13539  lss1d  14145  tgval2  14523  epttop  14562  cnnei  14704  txuni2  14728  txbas  14730  txdis1cn  14750  xmeterval  14907  dedekindicc  15105  plyun0  15208  lgslem3  15479  bj-stan  15683  nnti  15929