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

Theorem mpbir2an 682
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 680 . 2 (𝜑𝜒)
51, 4mpbir 221 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 382
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 197  df-an 383
This theorem is referenced by:  3pm3.2i  1422  eqssi  3766  elini  3946  dtru  4985  opnzi  5070  so0  5203  we0  5244  difxp  5699  ord0  5920  dfiota4  6022  funi  6063  funcnvsn  6079  fnresi  6148  fn0  6151  f0  6226  fconst  6231  f10  6310  f1o0  6314  f1oi  6315  f1osn  6317  isoid  6721  porpss  7087  ordon  7128  omssnlim  7225  fo1st  7334  fo2nd  7335  wfrfun  7577  wfr1  7585  iordsmo  7606  tfrlem7  7631  tfr1  7645  frfnom  7682  seqomlem2  7698  oawordeulem  7787  mapsnf1o2  8058  canth2  8268  unfilem2  8380  cantnfvalf  8725  cnfcom3clem  8765  tc2  8781  r111  8801  rankf  8820  cardf2  8968  harcard  9003  r0weon  9034  infxpenc  9040  infxpenc2lem1  9041  alephon  9091  alephf1  9107  alephiso  9120  alephsmo  9124  alephf1ALT  9125  alephfplem4  9129  ackbij1lem17  9259  ackbij1  9261  ackbij2  9266  isfin1-3  9409  fin1a2lem2  9424  fin1a2lem4  9426  axcc2lem  9459  iunfo  9562  smobeth  9609  0tsk  9778  1pi  9906  nqerf  9953  axaddf  10167  axmulf  10168  axicn  10172  mulnzcnopr  10874  negiso  11204  dfnn2  11234  nnind  11239  0z  11589  dfuzi  11669  cnref1o  12029  elrpii  12037  0e0icopnf  12488  0e0iccpnf  12489  fz0to4untppr  12649  fldiv4p1lem1div2  12843  om2uzf1oi  12959  om2uzisoi  12960  uzrdgfni  12964  expcl2lem  13078  expclzlem  13090  expge0  13102  expge1  13103  faclbnd4lem1  13283  hashkf  13322  wwlktovf1  13909  sqrtf  14310  fclim  14491  eff2  15034  reeff1  15055  ef01bndlem  15119  sin01bnd  15120  cos01bnd  15121  sin01gt0  15125  egt2lt3  15139  qnnen  15147  ruc  15177  halfleoddlt  15293  divalglem2  15325  divalglem9  15331  bitsf1  15375  sadaddlem  15395  2prm  15611  3prm  15612  1arith  15837  prmlem1a  16019  setsnid  16121  xpsff1o  16435  dmaf  16905  cdaf  16906  coapm  16927  isdrs2  17146  0pos  17161  isposi  17163  fpwipodrs  17371  letsr  17434  sgrp0b  17499  frmdplusg  17598  symg2bas  18024  pmtrsn  18145  odf  18162  efgsfo  18358  efgrelexlemb  18369  isabli  18413  mgpf  18766  prdscrngd  18820  xrsmgmdifsgrp  19997  xrs1cmn  20000  cnmgpid  20022  zringnzr  20044  zringunit  20050  zringlpir  20051  zringndrg  20052  zzngim  20115  cnmsgngrp  20139  psgninv  20142  zrhpsgnmhm  20144  retos  20180  refld  20181  pjpm  20268  fntopon  20948  istpsi  20966  0cmp  21417  cmpfi  21431  indisconn  21441  comppfsc  21555  kqf  21770  ptcmpfi  21836  fbssfi  21860  zfbas  21919  alexsubALTlem2  22071  alexsubALTlem4  22073  ptcmplem2  22076  ptcmp  22081  prdstmdd  22146  tsmsfbas  22150  ismeti  22349  prdsxmslem2  22553  cnfldms  22798  cnnrg  22803  tgqioo  22822  xrtgioo  22828  recld2  22836  xrge0gsumle  22855  xrge0tsms  22856  addcnlem  22886  divcn  22890  abscncf  22923  recncf  22924  imcncf  22925  cjcncf  22926  icopnfhmeo  22961  xrhmeo  22964  cnllycmp  22974  isclmi0  23116  iscvsi  23147  cnstrcvs  23159  cncvs  23163  cncms  23369  ovolf  23469  ovolicc1  23503  ovolre  23512  ioorf  23560  opnmblALT  23590  dveflem  23961  mdegxrf  24047  iaa  24299  ulmdm  24366  dvradcnv  24394  reeff1o  24420  reefiso  24421  reefgim  24423  recosf1o  24501  efifo  24513  rzgrp  24520  logcn  24613  cxpcn3  24709  resqrtcn  24710  logb1  24727  logbmpt  24746  ressatans  24881  lgamcvg2  25001  lgam1  25010  gam1  25011  efnnfsumcl  25049  efchtdvds  25105  ppiub  25149  lgslem2  25243  lgsfcl2  25248  lgsne0  25280  2lgslem1b  25337  padicabvf  25540  istrkg3ld  25580  axlowdimlem16  26057  upgrbi  26208  umgrbi  26216  lfuhgr1v0e  26368  cusgr0  26556  wlk2v2elem2  27333  upgr4cycl4dv4e  27362  konigsberglem4  27432  frgr0  27443  ex-pss  27621  ex-fl  27640  isgrpoi  27686  grporn  27709  isabloi  27739  smcnlem  27886  lnocoi  27946  cncph  28008  cnbn  28059  cnchl  28106  norm3adifii  28339  hhph  28369  hhhl  28395  hlim0  28426  hlimf  28428  helch  28434  hsn0elch  28439  hhssabloilem  28452  hhssnv  28455  hhshsslem2  28459  hhssbn  28471  hhsshl  28472  shscli  28510  shintcli  28522  chintcli  28524  shsval2i  28580  pjhthlem2  28585  lejdii  28731  nonbooli  28844  pjrni  28895  pjfoi  28896  pjfi  28897  pjmf1  28909  df0op2  28945  idunop  29171  0cnop  29172  0cnfn  29173  idcnop  29174  idhmop  29175  0hmop  29176  0lnfn  29178  0bdop  29186  lnophsi  29194  lnopcoi  29196  lnopunii  29205  lnophmi  29211  nmcopex  29222  nmcoplb  29223  nmcfnex  29246  nmcfnlb  29247  imaelshi  29251  nlelshi  29253  nlelchi  29254  riesz4i  29256  riesz4  29257  riesz1  29258  cnlnadjlem6  29265  cnlnadjlem9  29268  cnlnadjeui  29270  cnlnadjeu  29271  nmopadji  29283  bdophsi  29289  bdopcoi  29291  nmopcoadji  29294  pjhmopi  29339  pjbdlni  29342  hmopidmchi  29344  mdslj1i  29512  rinvf1o  29766  nnindf  29899  rpdp2cl  29923  dp2ltc  29928  dpmul4  29956  xrstos  30013  xrsclat  30014  xrge0omnd  30045  xrge0tsmsd  30119  reofld  30174  nn0archi  30177  xrge0iifmhm  30319  xrge0pluscn  30320  cnzh  30348  rezh  30349  qqhval2lem  30359  esum0  30445  esumcst  30459  esumpcvgval  30474  esumcvg  30482  dmvlsiga  30526  measdivcstOLD  30621  eulerpartlemt  30767  coinfliprv  30878  ballotlem2  30884  signswmnd  30968  logdivsqrle  31062  hgt750lem  31063  bnj906  31332  indispconn  31548  cnllysconn  31559  rellysconn  31565  msrf  31771  soseq  32085  frrlem5c  32117  bdayfo  32159  scutf  32250  brbigcup  32336  fobigcup  32338  brsingle  32355  fnsingle  32357  brimage  32364  funimage  32366  fnimage  32367  imageval  32368  brcart  32370  brapply  32376  brcup  32377  brcap  32378  funpartfun  32381  brub  32392  onsucconni  32767  onsucsuccmpi  32773  dnicn  32813  bj-dtru  33127  bj-rabtr  33252  bj-rabtrALTALT  33254  taupilem2  33498  taupi  33499  f1omptsnlem  33513  icoreresf  33530  relowlpssretop  33542  finxpreclem3  33560  matunitlindf  33733  mblfinlem2  33773  areacirc  33830  0totbnd  33897  heiborlem6  33940  refrelid  34606  idsymrel  34642  isolatiN  35018  isomliN  35041  ishlatiN  35157  mzpclall  37809  jm2.20nn  38083  dfacbasgrp  38197  dgraaf  38236  ifpim3  38360  ifpim4  38362  ifpbi1b  38367  iso0  39025  dvsid  39049  halffl  40021  resincncf  40600  0cnf  40602  iblempty  40692  dirkeritg  40830  fourierdlem62  40896  fourierdlem76  40910  fourierdlem103  40937  etransclem18  40980  etransclem46  41008  abnotbtaxb  41596  fmtnof1  41965  fmtno4prm  42005  prmdvdsfmtnof1  42017  31prm  42030  0evenALTV  42117  1oddALTV  42119  2evenALTV  42121  6even  42138  8even  42140  6gbe  42177  7gbow  42178  8gbe  42179  9gbo  42180  11gbo  42181  sprsymrelf1  42264  uspgrsprf1  42273  1odd  42329  nnsgrp  42335  0even  42449  2even  42451  2zrngamgm  42457  2zrngasgrp  42458  2zrngamnd  42459  2zrngagrp  42461  2zrngmsgrp  42465  zlmodzxzldeplem3  42809  lvecpsslmod  42814  ldepsnlinc  42815  blennngt2o2  42904  blennn0e2  42906  setrec2lem2  42959  aacllem  43068
  Copyright terms: Public domain W3C validator