HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem anbi12i 481
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
StepHypRef Expression
1 anbi12.1 . . 3 |- (ph <-> ps)
21anbi1i 480 . 2 |- ((ph /\ ch) <-> (ps /\ ch))
3 anbi12.2 . . 3 |- (ch <-> th)
43anbi2i 479 . 2 |- ((ps /\ ch) <-> (ps /\ th))
52, 4bitr 173 1 |- ((ph /\ ch) <-> (ps /\ th))
Colors of variables: wff set class
Syntax hints:   <-> wb 146   /\ wa 223
This theorem is referenced by:  pm4.11 520  con2bi 523  ordir 595  jcab 596  andi 602  orddi 604  pm5.17 666  dfbi 668  rnlem 771  3anbi123i 820  an6 899  19.43 1084  sbbi 1234  eu1 1385  euan 1421  2exeu 1439  2eu1 1442  2eu4 1445  2eu6 1447  sbabel 1576  neanior 1631  r19.26 1742  r19.26m 1744  r19.29 1748  reeanv 1770  reu2 1920  reu6 1922  eqss 2067  pssn2lp 2137  unss 2194  ssin 2222  undi 2242  inab 2258  reuss2 2265  reupick 2269  ralpr 2418  rexpr 2419  difprsn 2456  prsspw 2471  uniin 2510  intun 2552  intpr 2553  ssext 2753  pweqb 2755  pwin 2814  pwundif 2817  efrn2lp 2919  wetrep 2932  onminex 3010  sucelon 3058  opelxp 3204  elxp3 3214  weinxp 3223  relun 3251  inopab 3258  inxp 3259  opelcog 3279  cnvco 3289  dmin 3307  dfima2 3389  intasym 3422  asymref 3423  asymrefOLD 3425  cnvin 3442  xpnz 3452  xp11 3463  relssdr 3499  cnvpo 3508  cnvso 3509  dffun4 3514  funun 3540  fun11 3548  fununi 3549  imadif 3560  fun 3626  fint 3635  fin 3636  f1cnv 3651  f1co 3652  foco 3667  f1o3 3679  f1oco 3692  fsn 3819  f1ofv 3862  isotr 3882  isotrALT 3883  tfrlem5 3900  tfrlem7 3902  elxp6 4086  dfoprab5 4099  foprab2 4103  dfer2 4246  ider 4253  eqer 4255  brecop 4290  th3qlem1 4298  oprec 4302  mapval2 4319  brsdom 4363  map1 4411  xpcomen 4419  xpassen 4421  sbthlem9 4435  sbthlem10 4436  sbthcl 4439  brsdom2 4441  mapenlem2 4470  xpmapenlem5 4480  mapunen 4482  ssenen 4484  axinf2 4596  zfinf 4598  scottexs 4690  scott0s 4691  kardex 4697  karden 4698  aceq5lem1 4707  aceq5lem3 4709  kmlem15 4751  brdom7disj 4776  genpass 5084  addcompr 5095  mulcompr 5097  distrlem3pr 5101  mulgt0sr 5186  elreal 5222  addcnsr 5225  mulcnsr 5226  ltresr 5230  ltsor 5233  axcnre 5258  1re 5407  infmsup 6015  infmxrcl 6033  zmin 6167  nnwos 6392  elfzuzb 6408  creur 6673  creui 6674  abs00 6777  cvganz 6861  cvganuz 6862  dffsum 6936  climmullem8 7063  isupivth 7225  ivth2OLD 7234  reef11 7349  ruclem15 7467  infxpidmlem7 7501  tgval2t 7559  fctop 7592  cctop 7594  bopcnlem1 7915  fsumcnlem 7923  bcthlem32 7964  ajfval 8400  spwval2 8577  cosh111lem3 8631  grothprim 8722  shscl 9196  sshjvalt 9235  sshjval3t 9241  chcon2 9302  chcon3 9304  spanun 9382  hosmvalt 9428  hodmvalt 9430  hfsmvalt 9431  5oalem7 9522  3oalem3 9526  adjbdlnt 9931  pjin2 10031  pjin3 10032  cvnbtwn4t 10126  mdslj1 10154  mdslj2 10155  mdslmd1 10164  mdsldmd1 10166  chrelat4 10208  irred 10229  cdj3lem3 10270  cdj3lem3b 10272  cdj3 10273  elghom 10289  symgoprab 10307  symgf 10310  symggrpiOLD 10311  symggrpi 10313
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 147  df-an 225
Copyright terms: Public domain