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  1332  xorcom  1399  trubifal  1427  truxortru  1430  truxorfal  1431  falxortru  1432  falxorfal  1433  nford  1578  nfand  1579  sbequ8  1858  sbanv  1901  sban  1971  sbbi  1975  sbnf2  1997  eu1  2067  2exeu  2134  2eu4  2135  sbabel  2363  neanior  2451  rexeqbii  2507  r19.26m  2625  reean  2663  reu5  2711  reu2  2949  reu3  2951  eqss  3195  unss  3334  ralunb  3341  ssin  3382  undi  3408  difundi  3412  indifdir  3416  inab  3428  difab  3429  reuss2  3440  reupick  3444  raaan  3553  prss  3775  tpss  3785  prsspw  3792  prneimg  3801  uniin  3856  intun  3902  intpr  3903  disjiun  4025  brin  4082  brdif  4083  ssext  4251  pweqb  4253  opthg2  4269  copsex4g  4277  opelopabsb  4291  eqopab2b  4311  pwin  4314  pofun  4344  wetrep  4392  ordwe  4609  wessep  4611  reg3exmidlemwe  4612  elxp3  4714  soinxp  4730  relun  4777  inopab  4795  difopab  4796  inxp  4797  opelco2g  4831  cnvco  4848  dmin  4871  restidsing  4999  intasym  5051  asymref  5052  cnvdif  5073  xpm  5088  xp11m  5105  dfco2  5166  relssdmrn  5187  cnvpom  5209  xpcom  5213  dffun4  5266  dffun4f  5271  funun  5299  funcnveq  5318  fun11  5322  fununi  5323  imadif  5335  imainlem  5336  imain  5337  fnres  5371  fnopabg  5378  fun  5427  fin  5441  dff1o2  5506  brprcneu  5548  fsn  5731  dff1o6  5820  isotr  5860  brabvv  5965  eqoprab2b  5977  fvmpopr2d  6056  dfoprab3  6246  poxp  6287  cnvoprab  6289  f1od2  6290  brtpos2  6306  tfrlem7  6372  dfer2  6590  eqer  6621  iinerm  6663  brecop  6681  eroveu  6682  erovlem  6683  oviec  6697  mapval2  6734  ixpin  6779  xpcomco  6882  xpassen  6886  ssenen  6909  sbthlemi10  7027  infmoti  7089  dfmq0qs  7491  dfplq0qs  7492  enq0enq  7493  enq0tr  7496  npsspw  7533  nqprdisj  7606  ltnqpr  7655  ltnqpri  7656  ltexprlemdisj  7668  addcanprg  7678  recexprlemdisj  7692  caucvgprprlemval  7750  addsrpr  7807  mulsrpr  7808  mulgt0sr  7840  addcnsr  7896  mulcnsr  7897  ltresr  7901  addvalex  7906  axcnre  7943  axpre-suploc  7964  supinfneg  9663  infsupneg  9664  xrnemnf  9846  xrnepnf  9847  elfzuzb  10088  fzass4  10131  hashfacen  10910  rexanre  11367  cbvprod  11704  infssuzex  12089  nnwosdc  12179  isprm3  12259  issubm  13047  issubmd  13049  0subm  13059  insubm  13060  isnsg2  13276  lss1d  13882  tgval2  14230  epttop  14269  cnnei  14411  txuni2  14435  txbas  14437  txdis1cn  14457  xmeterval  14614  dedekindicc  14812  plyun0  14915  lgslem3  15159  bj-stan  15309  nnti  15555