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  1581  nfand  1582  sbequ8  1861  sbanv  1904  sban  1974  sbbi  1978  sbnf2  2000  eu1  2070  2exeu  2137  2eu4  2138  sbabel  2366  neanior  2454  rexeqbii  2510  r19.26m  2628  reean  2666  reu5  2714  reu2  2952  reu3  2954  eqss  3198  unss  3337  ralunb  3344  ssin  3385  undi  3411  difundi  3415  indifdir  3419  inab  3431  difab  3432  reuss2  3443  reupick  3447  raaan  3556  prss  3778  tpss  3788  prsspw  3795  prneimg  3804  uniin  3859  intun  3905  intpr  3906  disjiun  4028  brin  4085  brdif  4086  ssext  4254  pweqb  4256  opthg2  4272  copsex4g  4280  opelopabsb  4294  eqopab2b  4314  pwin  4317  pofun  4347  wetrep  4395  ordwe  4612  wessep  4614  reg3exmidlemwe  4615  elxp3  4717  soinxp  4733  relun  4780  inopab  4798  difopab  4799  inxp  4800  opelco2g  4834  cnvco  4851  dmin  4874  restidsing  5002  intasym  5054  asymref  5055  cnvdif  5076  xpm  5091  xp11m  5108  dfco2  5169  relssdmrn  5190  cnvpom  5212  xpcom  5216  dffun4  5269  dffun4f  5274  funun  5302  funcnveq  5321  fun11  5325  fununi  5326  imadif  5338  imainlem  5339  imain  5340  fnres  5374  fnopabg  5381  fun  5430  fin  5444  dff1o2  5509  brprcneu  5551  fsn  5734  dff1o6  5823  isotr  5863  brabvv  5968  eqoprab2b  5980  fvmpopr2d  6059  dfoprab3  6249  poxp  6290  cnvoprab  6292  f1od2  6293  brtpos2  6309  tfrlem7  6375  dfer2  6593  eqer  6624  iinerm  6666  brecop  6684  eroveu  6685  erovlem  6686  oviec  6700  mapval2  6737  ixpin  6782  xpcomco  6885  xpassen  6889  ssenen  6912  sbthlemi10  7032  infmoti  7094  dfmq0qs  7496  dfplq0qs  7497  enq0enq  7498  enq0tr  7501  npsspw  7538  nqprdisj  7611  ltnqpr  7660  ltnqpri  7661  ltexprlemdisj  7673  addcanprg  7683  recexprlemdisj  7697  caucvgprprlemval  7755  addsrpr  7812  mulsrpr  7813  mulgt0sr  7845  addcnsr  7901  mulcnsr  7902  ltresr  7906  addvalex  7911  axcnre  7948  axpre-suploc  7969  supinfneg  9669  infsupneg  9670  xrnemnf  9852  xrnepnf  9853  elfzuzb  10094  fzass4  10137  infssuzex  10323  hashfacen  10928  rexanre  11385  cbvprod  11723  nnwosdc  12206  isprm3  12286  issubm  13104  issubmd  13106  0subm  13116  insubm  13117  isnsg2  13333  lss1d  13939  tgval2  14287  epttop  14326  cnnei  14468  txuni2  14492  txbas  14494  txdis1cn  14514  xmeterval  14671  dedekindicc  14869  plyun0  14972  lgslem3  15243  bj-stan  15393  nnti  15639