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  822  orddi  825  3anbi123i  1212  an6  1355  xorcom  1430  trubifal  1458  truxortru  1461  truxorfal  1462  falxortru  1463  falxorfal  1464  nford  1613  nfand  1614  sbequ8  1893  sbanv  1936  sban  2006  sbbi  2010  sbnf2  2032  eu1  2102  2exeu  2170  2eu4  2171  sbabel  2399  neanior  2487  rexeqbii  2543  r19.26m  2662  reean  2700  reu5  2749  cbvreuw  2760  reu2  2991  reu3  2993  eqss  3239  unss  3378  ralunb  3385  ssin  3426  undi  3452  difundi  3456  indifdir  3460  inab  3472  difab  3473  reuss2  3484  reupick  3488  raaan  3597  prss  3823  tpss  3835  prsspw  3842  prneimg  3851  uniin  3907  intun  3953  intpr  3954  disjiun  4077  brin  4135  brdif  4136  ssext  4306  pweqb  4308  opthg2  4324  copsex4g  4332  opelopabsb  4347  eqopab2b  4367  pwin  4372  pofun  4402  wetrep  4450  ordwe  4667  wessep  4669  reg3exmidlemwe  4670  elxp3  4772  soinxp  4788  relun  4835  inopab  4853  difopab  4854  inxp  4855  opelco2g  4889  cnvco  4906  dmin  4930  restidsing  5060  intasym  5112  asymref  5113  cnvdif  5134  xpm  5149  xp11m  5166  dfco2  5227  relssdmrn  5248  cnvpom  5270  xpcom  5274  dffun4  5328  dffun4f  5333  funun  5361  funcnveq  5383  fun11  5387  fununi  5388  imadif  5400  imainlem  5401  imain  5402  fnres  5439  fnopabg  5446  fun  5496  fin  5511  dff1o2  5576  brprcneu  5619  fsn  5806  dff1o6  5899  isotr  5939  brabvv  6049  eqoprab2b  6061  fvmpopr2d  6140  dfoprab3  6335  poxp  6376  cnvoprab  6378  f1od2  6379  brtpos2  6395  tfrlem7  6461  dfer2  6679  eqer  6710  iinerm  6752  brecop  6770  eroveu  6771  erovlem  6772  oviec  6786  mapval2  6823  ixpin  6868  xpcomco  6981  xpassen  6985  ssenen  7008  sbthlemi10  7129  infmoti  7191  dfmq0qs  7612  dfplq0qs  7613  enq0enq  7614  enq0tr  7617  npsspw  7654  nqprdisj  7727  ltnqpr  7776  ltnqpri  7777  ltexprlemdisj  7789  addcanprg  7799  recexprlemdisj  7813  caucvgprprlemval  7871  addsrpr  7928  mulsrpr  7929  mulgt0sr  7961  addcnsr  8017  mulcnsr  8018  ltresr  8022  addvalex  8027  axcnre  8064  axpre-suploc  8085  supinfneg  9786  infsupneg  9787  xrnemnf  9969  xrnepnf  9970  elfzuzb  10211  fzass4  10254  infssuzex  10448  hashfacen  11053  rexanre  11726  cbvprod  12064  nnwosdc  12555  isprm3  12635  issubm  13500  issubmd  13502  0subm  13512  insubm  13513  isnsg2  13735  lss1d  14341  tgval2  14719  epttop  14758  cnnei  14900  txuni2  14924  txbas  14926  txdis1cn  14946  xmeterval  15103  dedekindicc  15301  plyun0  15404  lgslem3  15675  bj-stan  16069  nnti  16315