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

Theorem mpbir2an 955
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 953 . 2 (𝜑𝜒)
51, 4mpbir 221 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384
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 386
This theorem is referenced by:  3pm3.2i  1238  eqssi  3617  elini  3795  dtru  4855  opnzi  4941  so0  5066  we0  5107  difxp  5556  ord0  5775  dfiota4  5877  funi  5918  funcnvsn  5934  fnresi  6006  fn0  6009  f0  6084  fconst  6089  f10  6167  f1o0  6171  f1oi  6172  f1osn  6174  isoid  6576  porpss  6938  ordon  6979  omssnlim  7076  fo1st  7185  fo2nd  7186  wfrfun  7422  wfr1  7430  iordsmo  7451  tfrlem7  7476  tfr1  7490  frfnom  7527  seqomlem2  7543  oawordeulem  7631  mapsnf1o2  7902  canth2  8110  unfilem2  8222  cantnfvalf  8559  cnfcom3clem  8599  tc2  8615  r111  8635  rankf  8654  cardf2  8766  harcard  8801  r0weon  8832  infxpenc  8838  infxpenc2lem1  8839  alephon  8889  alephf1  8905  alephiso  8918  alephsmo  8922  alephf1ALT  8923  alephfplem4  8927  ackbij1lem17  9055  ackbij1  9057  ackbij2  9062  isfin1-3  9205  fin1a2lem2  9220  fin1a2lem4  9222  axcc2lem  9255  iunfo  9358  smobeth  9405  0tsk  9574  1pi  9702  nqerf  9749  axaddf  9963  axmulf  9964  axicn  9968  mulnzcnopr  10670  negiso  11000  dfnn2  11030  nnind  11035  0z  11385  dfuzi  11465  cnref1o  11824  elrpii  11832  0e0icopnf  12279  0e0iccpnf  12280  fz0to4untppr  12438  fldiv4p1lem1div2  12631  om2uzf1oi  12747  om2uzisoi  12748  uzrdgfni  12752  expcl2lem  12867  expclzlem  12879  expge0  12891  expge1  12892  faclbnd4lem1  13075  hashkf  13114  wwlktovf1  13694  sqrtf  14097  fclim  14278  eff2  14823  reeff1  14844  ef01bndlem  14908  sin01bnd  14909  cos01bnd  14910  sin01gt0  14914  egt2lt3  14928  qnnen  14936  ruc  14966  halfleoddlt  15080  divalglem2  15112  divalglem9  15118  bitsf1  15162  sadaddlem  15182  2prm  15399  3prm  15400  1arith  15625  prmlem1a  15807  setsnid  15909  xpsff1o  16222  dmaf  16693  cdaf  16694  coapm  16715  isdrs2  16933  0pos  16948  isposi  16950  fpwipodrs  17158  letsr  17221  sgrp0b  17286  frmdplusg  17385  symg2bas  17812  pmtrsn  17933  odf  17950  efgsfo  18146  efgrelexlemb  18157  isabli  18201  mgpf  18553  prdscrngd  18607  xrsmgmdifsgrp  19777  xrs1cmn  19780  cnmgpid  19802  zringnzr  19824  zringunit  19830  zringlpir  19831  zringndrg  19832  zzngim  19895  cnmsgngrp  19919  psgninv  19922  zrhpsgnmhm  19924  retos  19958  refld  19959  pjpm  20046  fntopon  20722  istpsi  20740  0cmp  21191  cmpfi  21205  indisconn  21215  comppfsc  21329  kqf  21544  ptcmpfi  21610  fbssfi  21635  zfbas  21694  alexsubALTlem2  21846  alexsubALTlem4  21848  ptcmplem2  21851  ptcmp  21856  prdstmdd  21921  tsmsfbas  21925  ismeti  22124  prdsxmslem2  22328  cnfldms  22573  cnnrg  22578  tgqioo  22597  xrtgioo  22603  recld2  22611  xrge0gsumle  22630  xrge0tsms  22631  addcnlem  22661  divcn  22665  abscncf  22698  recncf  22699  imcncf  22700  cjcncf  22701  icopnfhmeo  22736  xrhmeo  22739  cnllycmp  22749  isclmi0  22892  iscvsi  22923  cnstrcvs  22935  cncvs  22939  cncms  23145  ovolf  23244  ovolicc1  23278  ovolre  23287  ioorf  23335  opnmblALT  23365  dveflem  23736  mdegxrf  23822  iaa  24074  ulmdm  24141  dvradcnv  24169  reeff1o  24195  reefiso  24196  reefgim  24198  recosf1o  24275  efifo  24287  rzgrp  24294  logcn  24387  cxpcn3  24483  resqrtcn  24484  logb1  24501  logbmpt  24520  ressatans  24655  lgamcvg2  24775  lgam1  24784  gam1  24785  efnnfsumcl  24823  efchtdvds  24879  ppiub  24923  lgslem2  25017  lgsfcl2  25022  lgsne0  25054  2lgslem1b  25111  padicabvf  25314  istrkg3ld  25354  axlowdimlem16  25831  upgrbi  25982  umgrbi  25990  lfuhgr1v0e  26140  cusgr0  26316  wlk2v2elem2  27009  upgr4cycl4dv4e  27038  konigsberglem4  27110  frgr0  27121  ex-pss  27269  ex-fl  27288  isgrpoi  27336  grporn  27359  isabloi  27389  smcnlem  27536  lnocoi  27596  cncph  27658  cnbn  27709  cnchl  27756  norm3adifii  27989  hhph  28019  hhhl  28045  hlim0  28076  hlimf  28078  helch  28084  hsn0elch  28089  hhssabloilem  28102  hhssnv  28105  hhshsslem2  28109  hhssbn  28121  hhsshl  28122  shscli  28160  shintcli  28172  chintcli  28174  shsval2i  28230  pjhthlem2  28235  lejdii  28381  nonbooli  28494  pjrni  28545  pjfoi  28546  pjfi  28547  pjmf1  28559  df0op2  28595  idunop  28821  0cnop  28822  0cnfn  28823  idcnop  28824  idhmop  28825  0hmop  28826  0lnfn  28828  0bdop  28836  lnophsi  28844  lnopcoi  28846  lnopunii  28855  lnophmi  28861  nmcopex  28872  nmcoplb  28873  nmcfnex  28896  nmcfnlb  28897  imaelshi  28901  nlelshi  28903  nlelchi  28904  riesz4i  28906  riesz4  28907  riesz1  28908  cnlnadjlem6  28915  cnlnadjlem9  28918  cnlnadjeui  28920  cnlnadjeu  28921  nmopadji  28933  bdophsi  28939  bdopcoi  28941  nmopcoadji  28944  pjhmopi  28989  pjbdlni  28992  hmopidmchi  28994  mdslj1i  29162  rinvf1o  29416  nnindf  29550  rpdp2cl  29574  dp2ltc  29579  dpmul4  29607  xrstos  29664  xrsclat  29665  xrge0omnd  29696  xrge0tsmsd  29770  reofld  29825  nn0archi  29828  xrge0iifmhm  29970  xrge0pluscn  29971  cnzh  29999  rezh  30000  qqhval2lem  30010  esum0  30096  esumcst  30110  esumpcvgval  30125  esumcvg  30133  dmvlsiga  30177  measdivcstOLD  30272  eulerpartlemt  30418  coinfliprv  30529  ballotlem2  30535  signswmnd  30619  logdivsqrle  30713  hgt750lem  30714  bnj906  30985  indispconn  31201  cnllysconn  31212  rellysconn  31218  msrf  31424  soseq  31735  frrlem5c  31770  bdayfo  31812  scutf  31903  brbigcup  31989  fobigcup  31991  brsingle  32008  fnsingle  32010  brimage  32017  funimage  32019  fnimage  32020  imageval  32021  brcart  32023  brapply  32029  brcup  32030  brcap  32031  funpartfun  32034  brub  32045  onsucconni  32420  onsucsuccmpi  32426  dnicn  32466  bj-dtru  32781  bj-rabtr  32910  bj-rabtrALTALT  32912  taupilem2  33148  taupi  33149  f1omptsnlem  33163  icoreresf  33180  relowlpssretop  33192  finxpreclem3  33210  matunitlindf  33387  mblfinlem2  33427  areacirc  33485  0totbnd  33552  heiborlem6  33595  isolatiN  34329  isomliN  34352  ishlatiN  34468  mzpclall  37116  jm2.20nn  37390  dfacbasgrp  37504  dgraaf  37543  ifpim3  37667  ifpim4  37669  ifpbi1b  37674  iso0  38332  dvsid  38356  halffl  39329  resincncf  39857  0cnf  39859  iblempty  39950  dirkeritg  40088  fourierdlem62  40154  fourierdlem76  40168  fourierdlem103  40195  etransclem18  40238  etransclem46  40266  abnotbtaxb  40851  fmtnof1  41218  fmtno4prm  41258  prmdvdsfmtnof1  41270  31prm  41283  0evenALTV  41370  1oddALTV  41372  2evenALTV  41374  6even  41391  8even  41393  6gbe  41430  7gbow  41431  8gbe  41432  9gbo  41433  11gbo  41434  sprsymrelf1  41517  uspgrsprf1  41526  1odd  41582  nnsgrp  41588  0even  41702  2even  41704  2zrngamgm  41710  2zrngasgrp  41711  2zrngamnd  41712  2zrngagrp  41714  2zrngmsgrp  41718  zlmodzxzldeplem3  42062  lvecpsslmod  42067  ldepsnlinc  42068  blennngt2o2  42157  blennn0e2  42159  setrec2lem2  42212  aacllem  42318
  Copyright terms: Public domain W3C validator