MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  anbi12i Unicode version

Theorem anbi12i 679
Description: Conjoin both sides of two equivalences. (Contributed by NM, 5-Aug-1993.)
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 677 . 2  |-  ( (
ph  /\  ch )  <->  ( ps  /\  ch )
)
3 anbi12.2 . . 3  |-  ( ch  <->  th )
43anbi2i 676 . 2  |-  ( ( ps  /\  ch )  <->  ( ps  /\  th )
)
52, 4bitri 241 1  |-  ( (
ph  /\  ch )  <->  ( ps  /\  th )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359
This theorem is referenced by:  anbi12ci  680  ordi  835  ordir  836  orddi  840  pm5.17  859  xor  862  3anbi123i  1142  an6  1263  nanbi  1300  cadan  1398  nic-axALT  1445  19.43OLD  1613  nfimdOLD  1824  sbbi  2128  sbnf2  2165  eu1  2283  2eu1  2342  2eu4  2345  2eu6  2347  sbabel  2574  neanior  2660  rexeqbii  2705  r19.26m  2809  reean  2842  2ralor  2845  reu5  2889  reu2  3090  reu3  3092  2reu5lem3  3109  eqss  3331  unss  3489  ralunb  3496  ssin  3531  undi  3556  indifdir  3565  undif3  3570  inab  3577  difab  3578  reuss2  3589  reupick  3593  prss  3920  sstp  3931  tpss  3932  prsspw  3939  prneimg  3946  prnebg  3947  uniin  4003  intun  4050  intpr  4051  disjiun  4170  disjxiun  4177  brin  4227  brdif  4228  ssext  4386  pweqb  4388  opthg2  4405  copsex4g  4413  eqopab2b  4452  pwin  4455  pofun  4487  wetrep  4543  sucelon  4764  elxp3  4895  soinxp  4909  weinxp  4912  relun  4958  inopab  4972  difopab  4973  inxp  4974  opelco2g  5007  cnvco  5023  dmin  5044  intasym  5216  asymref  5217  asymref2  5218  cnvdif  5245  xpnz  5259  xp11  5271  dfco2  5336  relssdmrn  5357  cnvpo  5377  cnvso  5378  xpco  5381  dffun4  5433  funun  5462  fun11  5483  fununi  5484  imadif  5495  fnres  5528  fnopabg  5535  fun  5574  fin  5590  dff1o2  5646  brprcneu  5688  dffv2  5763  fsn  5873  dff1o6  5980  isotr  6023  eqoprab2b  6099  elxp6  6345  difxp  6347  dfoprab3  6370  fsplit  6418  poxp  6425  soxp  6426  brtpos2  6452  porpss  6493  opiota  6502  tfrlem5  6608  tfrlem7  6611  dfer2  6873  eqer  6905  iiner  6943  uniinqs  6951  brecop  6964  eroveu  6966  erovlem  6967  ovec  6981  mapval2  7010  ixpin  7054  boxriin  7071  brsdom  7097  xpcomco  7165  xpassen  7169  sbthlem9  7192  sbthlem10  7193  brsdom2  7198  ssenen  7248  unfi  7341  dffi3  7402  dfsup2  7413  dfsup2OLD  7414  axinf2  7559  zfinf2  7561  oemapso  7602  scottexs  7775  scott0s  7776  kardex  7782  karden  7783  dfac5lem1  7968  dfac5lem3  7970  kmlem15  8008  enfin2i  8165  fin23lem34  8190  brdom7disj  8373  fpwwe2lem12  8480  fpwwe2lem13  8481  axgroth5  8663  grothprim  8673  mulgt0sr  8944  addcnsr  8974  mulcnsr  8975  ltresr  8979  axcnre  9003  1re  9054  ssxr  9109  infmsup  9950  infmrgelb  9952  infmrlb  9953  nnwos  10508  zmin  10534  xrnemnf  10682  xrnepnf  10683  xmullem  10807  xmulcom  10809  xmulneg1  10812  xmulf  10815  xrinfmss2  10853  elfzuzb  11017  fzass4  11054  seqof  11343  hashbclem  11664  hashfacen  11666  rexanre  12113  caubnd  12125  o1lo1  12294  rpnnen2  12788  isprm3  13051  prmreclem2  13248  4sqlem12  13287  isffth2  14076  fucinv  14133  lubid  14402  oduglb  14529  odulub  14531  issubm  14711  isnsg2  14933  oppgid  15115  lsmdisjr  15279  lsmhash  15300  dprd0  15552  dvdsrtr  15720  isirred2  15769  lss1d  16002  lspsolvlem  16177  lbsextlem2  16194  unocv  16870  iunocv  16871  tgval2  16984  fctop  17031  cctop  17033  ppttop  17034  epttop  17036  cnnei  17308  2ndcctbss  17479  txuni2  17558  txbas  17560  ptbasin  17570  txdis1cn  17628  xkococnlem  17652  opnfbas  17835  fgcl  17871  fbasrn  17877  filuni  17878  cfinfil  17886  csdfil  17887  fin1aufil  17925  rnelfmlem  17945  fmfnfmlem3  17949  txflf  17999  xmeterval  18423  reconn  18820  iimulcl  18923  iscau3  19192  minveclem3  19291  pmltpc  19308  ovolfcl  19324  ismbl  19383  dyaddisj  19449  iblre  19646  evlsval  19901  plyun0  20077  logfaclbnd  20967  lgslem3  21043  lgsdir2lem5  21072  nb3grapr2  21424  cusgra3v  21434  4cycl4v4e  21614  4cycl4dv4e  21616  elghom  21912  ajfval  22271  issh  22671  chcon2i  22927  chcon3i  22929  spanuni  23007  5oalem7  23123  3oalem3  23127  pjin2i  23657  pjin3i  23658  cvnbtwn4  23753  mdslj1i  23783  mdslj2i  23784  mdslmd1i  23793  chrelat4i  23837  chirredi  23858  cdj3i  23905  iuninc  23972  suppss2f  24010  fmptdF  24030  mptfnf  24034  disjdsct  24051  tosglb  24153  esumpfinvalf  24427  measiuns  24532  sibfof  24615  ballotlem2  24707  ballotlemodife  24716  derangenlem  24818  pconcon  24879  dftr6  25329  dffr5  25332  dfpo2  25334  fundmpss  25344  elpotr  25359  soseq  25476  wfrlem5  25482  wfrlem11  25488  frrlem5  25507  frrlem5c  25509  nocvxmin  25567  brtxp  25642  brpprod  25647  brsset  25651  idsset  25652  dfon3  25654  ellimits  25672  elfuns  25676  brcart  25693  brapply  25699  brcap  25701  brsuccf  25702  funpartfun  25704  dfrdg4  25711  tfrqfree  25712  altopthc  25728  altopthd  25729  altopelaltxp  25733  outsideoftr  25975  df3nandALT1  26058  imnand2  26061  ismblfin  26154  mbfposadd  26161  trer  26217  gtinf  26220  neibastop1  26286  neifg  26298  inixp  26328  keridl  26540  smprngopr  26560  prtlem10  26612  prter1  26626  mzpclall  26682  mzpincl  26689  mzpindd  26701  2nn0ind  26906  dford4  26998  wopprc  26999  islmodfg  27043  issubmd  27259  gsumcom3  27330  isdomn3  27399  2reu5a  27830  2reu1  27839  2reu4a  27842  f13dfv  27970  frisusgranb  28109  frgra3v  28114  onfrALTlem5  28347  onfrALTlem4  28348  undif3VD  28712  onfrALTlem5VD  28715  onfrALTlem4VD  28716  bnj887  28852  bnj976  28866  bnj1385  28922  bnj153  28969  bnj543  28982  bnj607  29005  bnj882  29015  bnj916  29022  bnj983  29040  sbbiNEW7  29286  sbnf2NEW7  29321  lcvbr3  29518  isopos  29675  llnexatN  30015  snatpsubN  30244  pclclN  30385  pclfinN  30394  lhpocnel2  30513  cdlemk19w  31466  dih1dimatlem  31824
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator