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  817  orddi  820  dcan  933  3anbi123i  1188  an6  1321  xorcom  1388  trubifal  1416  truxortru  1419  truxorfal  1420  falxortru  1421  falxorfal  1422  nford  1567  nfand  1568  sbequ8  1847  sbanv  1889  sban  1955  sbbi  1959  sbnf2  1981  eu1  2051  2exeu  2118  2eu4  2119  sbabel  2346  neanior  2434  rexeqbii  2490  r19.26m  2608  reean  2645  reu5  2689  reu2  2925  reu3  2927  eqss  3170  unss  3309  ralunb  3316  ssin  3357  undi  3383  difundi  3387  indifdir  3391  inab  3403  difab  3404  reuss2  3415  reupick  3419  raaan  3529  prss  3748  tpss  3757  prsspw  3764  prneimg  3773  uniin  3828  intun  3874  intpr  3875  disjiun  3996  brin  4053  brdif  4054  ssext  4219  pweqb  4221  opthg2  4237  copsex4g  4245  opelopabsb  4258  eqopab2b  4277  pwin  4280  pofun  4310  wetrep  4358  ordwe  4573  wessep  4575  reg3exmidlemwe  4576  elxp3  4678  soinxp  4694  relun  4741  inopab  4756  difopab  4757  inxp  4758  opelco2g  4792  cnvco  4809  dmin  4832  restidsing  4960  intasym  5010  asymref  5011  cnvdif  5032  xpm  5047  xp11m  5064  dfco2  5125  relssdmrn  5146  cnvpom  5168  xpcom  5172  dffun4  5224  dffun4f  5229  funun  5257  funcnveq  5276  fun11  5280  fununi  5281  imadif  5293  imainlem  5294  imain  5295  fnres  5329  fnopabg  5336  fun  5385  fin  5399  dff1o2  5463  brprcneu  5505  fsn  5685  dff1o6  5772  isotr  5812  brabvv  5916  eqoprab2b  5928  dfoprab3  6187  poxp  6228  cnvoprab  6230  f1od2  6231  brtpos2  6247  tfrlem7  6313  dfer2  6531  eqer  6562  iinerm  6602  brecop  6620  eroveu  6621  erovlem  6622  oviec  6636  mapval2  6673  ixpin  6718  xpcomco  6821  xpassen  6825  ssenen  6846  sbthlemi10  6960  infmoti  7022  dfmq0qs  7423  dfplq0qs  7424  enq0enq  7425  enq0tr  7428  npsspw  7465  nqprdisj  7538  ltnqpr  7587  ltnqpri  7588  ltexprlemdisj  7600  addcanprg  7610  recexprlemdisj  7624  caucvgprprlemval  7682  addsrpr  7739  mulsrpr  7740  mulgt0sr  7772  addcnsr  7828  mulcnsr  7829  ltresr  7833  addvalex  7838  axcnre  7875  axpre-suploc  7896  supinfneg  9589  infsupneg  9590  xrnemnf  9771  xrnepnf  9772  elfzuzb  10012  fzass4  10055  hashfacen  10807  rexanre  11220  cbvprod  11557  infssuzex  11940  nnwosdc  12030  isprm3  12108  issubm  12791  issubmd  12793  0subm  12799  insubm  12800  tgval2  13333  epttop  13372  cnnei  13514  txuni2  13538  txbas  13540  txdis1cn  13560  xmeterval  13717  dedekindicc  13893  lgslem3  14185  bj-stan  14270  nnti  14515