Theorem anbi12i 540

Description: Conjoin both sides of two equivalences.

Hypotheses

Ref	Expression
anbi12.1	|- (ph <-> ps)
anbi12.2	|- (ch <-> th)

Assertion

Ref	Expression
anbi12i	|- ((ph /\ ch) <-> (ps /\ th))

Proof of Theorem anbi12i

Step	Hyp	Ref	Expression
1		anbi12.1	. . 3 |- (ph <-> ps)
2	1	anbi1i 539	. 2 |- ((ph /\ ch) <-> (ps /\ ch))
3		anbi12.2	. . 3 |- (ch <-> th)
4	3	anbi2i 538	. 2 |- ((ps /\ ch) <-> (ps /\ th))
5	2, 4	bitri 190	1 |- ((ph /\ ch) <-> (ps /\ th))

Syntax hints:   <-> wb 163   /\ wa 240

This theorem is referenced by:  notbi 581  con2bi 584  ordir 658  jcab 659  andi 665  orddi 667  bibi2i 669  pm5.17 731  dfbi3 733  rnlemOLD 854  3anbi123i 1056  an6 1177  nic-justbi 1234  nic-axALT 1240  19.43 1440  sbbi 1609  eu1 1786  euanOLD 1828  2exeu 1850  2eu1 1853  2eu4 1856  2eu6 1858  sbabel 2016  neanior 2097  r19.26OLD 2220  r19.26m 2222  r19.29OLD 2228  reean 2247  reeanOLD 2248  2ralor 2250  reu2 2442  reu3 2444  difjustOLD 2596  injustOLD 2602  eqss 2631  pssn2lpOLD 2710  unss 2780  ralunb 2784  ssin 2814  ssinOLD 2815  undi 2840  undiOLD 2841  undif3 2854  inab 2861  inabOLD 2862  difab 2863  reuss2 2870  reupick 2874  sbsslemOLD 2979  ralprOLD 3080  ralprOLDOLD 3081  rexpr 3082  difprsn 3127  difprsnOLD 3128  prss 3138  tpss 3145  prsspw 3150  prsspwOLD 3151  uniin 3197  uniinOLD 3198  intun 3249  intpr 3250  brin 3388  brdif 3389  ssext 3508  pweqb 3511  opelopabsb 3564  pwin 3576  pwundif 3579  efrn2lp 3638  wetrep 3651  onminex 3888  sucelon 3898  opelxpOLD 4037  elxp3 4049  weinxp 4059  relun 4097  inopab 4108  inxp 4109  inxpOLD 4110  opelco2g 4133  cnvco 4145  cnvcoOLD 4146  dmin 4165  dfima2OLD 4266  intasym 4306  intasymOLD 4307  asymref 4308  asymrefOLD 4309  asymref2 4310  cnvin 4324  xpnz 4335  xp11 4347  dfco2 4393  relssdmrn 4416  cnvpo 4427  cnvso 4428  dffun4 4433  funun 4462  fun11 4480  fununi 4481  imadif 4493  fco 4573  fun 4580  fintOLD 4592  fin 4593  finOLD 4594  f1cnv 4611  f1co 4612  foco 4628  dff1o2 4639  dff1o3OLD 4642  f1oco 4661  dffv2 4734  fsn 4807  dff1o6 4853  isotr 4874  isotrALT 4875  elxp6 5041  dfoprab3s 5055  dfoprab5sf 5058  foprab2 5061  fparlem3 5083  fparlem4 5084  fsplit 5086  tfrlem5 5123  tfrlem7 5125  dfer2 5319  iderOLD 5327  eqer 5329  brecop 5365  th3qlem1 5373  oprec 5377  mapval2 5394  brsdom 5440  map1 5489  xpcomen 5498  xpassen 5500  sbthlem9 5518  sbthlem10 5519  sbthcl 5522  brsdom2 5524  mapenlem2 5584  xpmapenlem5 5594  mapunen 5596  ssenen 5598  unfi 5644  axinf2 5730  zfinf2 5732  scottexs 5848  scott0s 5849  kardex 5855  karden 5856  aceq5lem1 5897  aceq5lem3 5899  kmlem15 5941  brdom7disj 5966  genpass 6264  addcompr 6275  mulcompr 6277  distrlem3pr 6281  mulgt0sr 6366  elreal 6402  addcnsr 6405  mulcnsr 6406  ltresr 6410  ltsor 6413  axcnre 6439  1re 6598  ssxr 6714  infmsup 7277  infmxrcl 7295  zmin 7432  nnwos 7629  elfzuzb 7646  fzprval 7687  creur 7992  creui 7993  abs00i 8093  cvganz 8176  cvganuzi 8177  dffsum 8258  climmullem8 8387  isupivthi 8552  reef11i 8673  ruclem15 8793  infxpidmlem7 8827  tgval2 8887  fctop 8920  cctop 8922  txbas 8933  bopcnlem1 9259  fsumcnlem 9267  bcthlem32 9308  gapm 9462  ajfval 9809  spwval2 9996  cosh111lem3 10070  axgroth5 10132  grothpw 10134  grothprim 10141  elghom 10195  symgoprab 10201  symgf 10204  symggrpi 10205  extbas1 10291  filrn 10293  isexid 10364  shscli 10914  sshjval 10953  sshjval3 10959  chcon2i 11020  chcon3i 11022  spanuni 11100  hosmval 11144  hodmval 11146  hfsmval 11147  5oalem7 11240  3oalem3 11244  adjbdln 11653  pjin2i 11766  pjin3i 11767  cvnbtwn4 11861  mdslj1i 11891  mdslj2i 11892  mdslmd1i 11901  mdsldmd1i 11903  chrelat4i 11945  irredi 11966  cdj3lem3 12010  cdj3lem3b 12012  cdj3i 12013  bnj186 12056  bnj193OLD 12064  bnj10OLD 12375  bnj18 12384  bnj34 12403  bnj887 12810  bnj912 12822  bnj971 12860  bnj1385 13102  bnj86 13213  bnj87 13214  bnj149 13241  bnj153 13247  bnj543 13269  bnj607 13304  bnj882 13320  bnj983 13357  bnj1043 13391  isprm3 13776  ralunbOLD 13819  indifdi 13823  dif2relOLD 13828  dffr5 13831  dftr6 13834  fundmpss 13836  mpteqi 13838  elpotr 13847  poxp 13949  soxp 13950  poseq 13954  soseq 13955  wfrlem5 13961  wfrlem11 13967  axsltsolem1 14006  nocvxmin 14029  axfelem11 14041  brtxp 14067  brsset 14069  idsset 14070  dfon3 14072  brbigcup 14074  ellimits 14079  df3nandALT1 14146  imnand2 14149  anddi2 14268  albineal 14323  dff1o6f 14416  omslim 14420  inposet 14620  definc 14621  dffprod 14670  vecval1b 14794  vecval3b 14795  trer 15361  fictb 15371  opncldf1 15402  dfcon2 15442  is1stc3 15469  2ndcctbss 15478  neibastop1 15518  opnfbas 15557  neifg 15559  filssufillem 15570  ufinffr 15578  ufilen 15579  rnelfmlem 15592  fmfnfmlem3 15596  filnetlem3 15642  filnetlem4 15643  2ralorOLD 15655  prfunOLD 15677  difxp 15690  inixp 15722  eroprlem 15732  eropreu 15733  eroprf 15735  infmrlb 15765  infmrgelb 15766  pofun 15772  fsum00 15820  iimulcl 15874  txcnoprab 15911  heiborlem20 15974  bfp 16009  phtpycom 16050  pcoloopf 16079  pi1fval 16092  pi1val 16094  keridl 16180  smprngpr 16200  prtlem5 16245  smores 16446  undif3VD 16706  strdif 16719  stb2xpl 16742  stb2str 16744  stb2v1 16745  stb2v2 16746  lubid 16807  grpstr 17097  cnaddablNEW 17139

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-an 242

Copyright terms: Public domain