MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpbir2an Structured version   Visualization version   GIF version

Theorem mpbir2an 957
Description: Detach a conjunction of truths in a biconditional. (Contributed by NM, 10-May-2005.)
Hypotheses
Ref Expression
mpbir2an.1 𝜓
mpbir2an.2 𝜒
mpbiran2an.1 (𝜑 ↔ (𝜓𝜒))
Assertion
Ref Expression
mpbir2an 𝜑

Proof of Theorem mpbir2an
StepHypRef Expression
1 mpbir2an.2 . 2 𝜒
2 mpbir2an.1 . . 3 𝜓
3 mpbiran2an.1 . . 3 (𝜑 ↔ (𝜓𝜒))
42, 3mpbiran 955 . 2 (𝜑𝜒)
51, 4mpbir 220 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wb 195  wa 383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 196  df-an 385
This theorem is referenced by:  3pm3.2i  1232  eqssi  3584  dtru  4783  opnzi  4869  so0  4992  we0  5033  difxp  5477  ord0  5694  funi  5834  funcnvsn  5850  fnresi  5922  fn0  5924  f0  5999  fconst  6004  f10  6081  f1o0  6085  f1oi  6086  f1osn  6088  isoid  6479  porpss  6839  ordon  6874  omssnlim  6971  fo1st  7079  fo2nd  7080  wfrfun  7312  wfr1  7320  iordsmo  7341  tfrlem7  7366  tfr1  7380  frfnom  7417  seqomlem2  7433  oawordeulem  7521  mapsnf1o2  7791  canth2  7998  unfilem2  8110  cantnfvalf  8445  cnfcom3clem  8485  tc2  8501  r111  8521  rankf  8540  cardf2  8652  harcard  8687  r0weon  8718  infxpenc  8724  infxpenc2lem1  8725  alephon  8775  alephf1  8791  alephiso  8804  alephsmo  8808  alephf1ALT  8809  alephfplem4  8813  ackbij1lem17  8941  ackbij1  8943  ackbij2  8948  isfin1-3  9091  fin1a2lem2  9106  fin1a2lem4  9108  axcc2lem  9141  iunfo  9240  smobeth  9287  0tsk  9456  1pi  9584  nqerf  9631  axaddf  9845  axmulf  9846  axicn  9850  mulnzcnopr  10552  negiso  10880  dfnn2  10910  nnind  10915  0z  11265  dfuzi  11344  cnref1o  11703  elrpii  11711  0e0icopnf  12153  0e0iccpnf  12154  fz0to4untppr  12311  fldiv4p1lem1div2  12498  om2uzf1oi  12614  om2uzisoi  12615  uzrdgfni  12619  expcl2lem  12734  expclzlem  12746  expge0  12758  expge1  12759  faclbnd4lem1  12942  hashkf  12981  wwlktovf1  13548  sqrtf  13951  fclim  14132  eff2  14668  reeff1  14689  ef01bndlem  14753  sin01bnd  14754  cos01bnd  14755  sin01gt0  14759  egt2lt3  14773  qnnen  14781  ruc  14811  halfleoddlt  14924  divalglem2  14956  divalglem9  14962  bitsf1  15006  sadaddlem  15026  2prm  15243  3prm  15244  1arith  15469  prmlem1a  15651  setsnid  15743  xpsff1o  16051  dmaf  16522  cdaf  16523  coapm  16544  isdrs2  16762  0pos  16777  isposi  16779  fpwipodrs  16987  letsr  17050  sgrp0b  17115  frmdplusg  17214  symg2bas  17641  pmtrsn  17762  odf  17779  efgsfo  17975  efgrelexlemb  17986  isabli  18030  mgpf  18382  prdscrngd  18436  xrsmgmdifsgrp  19602  xrs1cmn  19605  cnmgpid  19627  zringnzr  19649  zringunit  19655  zringlpir  19656  zringndrg  19657  zzngim  19720  cnmsgngrp  19744  psgninv  19747  zrhpsgnmhm  19749  retos  19783  refld  19784  pjpm  19871  istpsi  20559  0cmp  21007  cmpfi  21021  indiscon  21031  comppfsc  21145  kqf  21360  ptcmpfi  21426  fbssfi  21451  zfbas  21510  alexsubALTlem2  21662  alexsubALTlem4  21664  ptcmplem2  21667  ptcmp  21672  prdstmdd  21737  tsmsfbas  21741  ismeti  21940  prdsxmslem2  22144  cnfldms  22389  cnnrg  22394  tgqioo  22411  xrtgioo  22417  recld2  22425  xrge0gsumle  22444  xrge0tsms  22445  addcnlem  22475  divcn  22479  abscncf  22512  recncf  22513  imcncf  22514  cjcncf  22515  icopnfhmeo  22550  xrhmeo  22553  cnllycmp  22563  isclmi0  22706  iscvsi  22737  cnstrcvs  22749  cncvs  22753  cncms  22959  ovolf  23057  ovolicc1  23091  ovolre  23100  ioorf  23147  opnmblALT  23177  dveflem  23546  mdegxrf  23632  iaa  23884  ulmdm  23951  dvradcnv  23979  reeff1o  24005  reefiso  24006  reefgim  24008  recosf1o  24085  efifo  24097  rzgrp  24104  logcn  24193  cxpcn3  24289  resqrtcn  24290  logb1  24307  logbmpt  24326  ressatans  24461  lgamcvg2  24581  lgam1  24590  gam1  24591  efnnfsumcl  24629  efchtdvds  24685  ppiub  24729  lgslem2  24823  lgsfcl2  24828  lgsne0  24860  2lgslem1b  24917  padicabvf  25120  istrkg3ld  25160  axlowdimlem16  25637  upgrbi  25760  umgrbi  25767  wlkntrllem2  26090  umgrabi  26510  konigsberg  26514  ex-pss  26677  ex-fl  26696  isgrpoi  26736  grporn  26759  isabloi  26789  smcnlem  26936  lnocoi  26996  cncph  27058  cnbn  27109  cnchl  27156  norm3adifii  27389  hhph  27419  hhhl  27445  hlim0  27476  hlimf  27478  helch  27484  hsn0elch  27489  hhssabloilem  27502  hhssnv  27505  hhshsslem2  27509  hhssbn  27521  hhsshl  27522  shscli  27560  shintcli  27572  chintcli  27574  shsval2i  27630  pjhthlem2  27635  lejdii  27781  nonbooli  27894  pjrni  27945  pjfoi  27946  pjfi  27947  pjmf1  27959  df0op2  27995  idunop  28221  0cnop  28222  0cnfn  28223  idcnop  28224  idhmop  28225  0hmop  28226  0lnfn  28228  0bdop  28236  lnophsi  28244  lnopcoi  28246  lnopunii  28255  lnophmi  28261  nmcopex  28272  nmcoplb  28273  nmcfnex  28296  nmcfnlb  28297  imaelshi  28301  nlelshi  28303  nlelchi  28304  riesz4i  28306  riesz4  28307  riesz1  28308  cnlnadjlem6  28315  cnlnadjlem9  28318  cnlnadjeui  28320  cnlnadjeu  28321  nmopadji  28333  bdophsi  28339  bdopcoi  28341  nmopcoadji  28344  pjhmopi  28389  pjbdlni  28392  hmopidmchi  28394  mdslj1i  28562  rinvf1o  28814  nnindf  28952  xrstos  29010  xrsclat  29011  xrge0omnd  29042  xrge0tsmsd  29116  reofld  29171  nn0archi  29174  xrge0iifmhm  29313  xrge0pluscn  29314  cnzh  29342  rezh  29343  qqhval2lem  29353  esum0  29438  esumcst  29452  esumpcvgval  29467  esumcvg  29475  dmvlsiga  29519  measdivcstOLD  29614  eulerpartlemt  29760  coinfliprv  29871  ballotlem2  29877  signswmnd  29960  bnj906  30254  indispcon  30470  cnllyscon  30481  rellyscon  30487  msrf  30693  soseq  30995  frrlem5c  31030  bdayfo  31074  bdayfn  31078  brbigcup  31175  fobigcup  31177  brsingle  31194  fnsingle  31196  brimage  31203  funimage  31205  fnimage  31206  imageval  31207  brcart  31209  brapply  31215  brcup  31216  brcap  31217  funpartfun  31220  brub  31231  onsucconi  31606  onsucsuccmpi  31612  dnicn  31652  bj-dtru  31985  bj-rabtr  32118  bj-rabtrALTALT  32120  bj-fntopon  32243  taupilem2  32345  taupi  32346  f1omptsnlem  32359  icoreresf  32376  relowlpssretop  32388  finxpreclem3  32406  matunitlindf  32577  mblfinlem2  32617  areacirc  32675  0totbnd  32742  heiborlem6  32785  isolatiN  33521  isomliN  33544  ishlatiN  33660  mzpclall  36308  jm2.20nn  36582  dfacbasgrp  36697  dgraaf  36736  ifpim3  36860  ifpim4  36862  ifpbi1b  36867  iso0  37528  dvsid  37552  halffl  38451  resincncf  38760  0cnf  38762  iblempty  38857  dirkeritg  38995  fourierdlem62  39061  fourierdlem76  39075  fourierdlem103  39102  etransclem18  39145  etransclem46  39173  abnotbtaxb  39731  fmtnof1  39985  fmtno4prm  40025  prmdvdsfmtnof1  40037  31prm  40050  0evenALTV  40137  1oddALTV  40139  2evenALTV  40141  6even  40158  8even  40160  6gbe  40193  7gbo  40194  8gbe  40195  9gboa  40196  11gboa  40197  lfuhgr1v0e  40480  cusgr0  40648  1wlk2v2elem2  41323  upgr4cycl4dv4e  41352  konigsberglem4  41425  frgr0  41436  1odd  41601  nnsgrp  41607  0even  41721  2even  41723  2zrngamgm  41729  2zrngasgrp  41730  2zrngamnd  41731  2zrngagrp  41733  2zrngmsgrp  41737  zlmodzxzldeplem3  42085  lvecpsslmod  42090  ldepsnlinc  42091  blennngt2o2  42184  blennn0e2  42186  setrec2lem2  42240  aacllem  42356
  Copyright terms: Public domain W3C validator