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

Theorem mpbir2an 975
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 973 . 2 (𝜑𝜒)
51, 4mpbir 221 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wb 196  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 197  df-an 385
This theorem is referenced by:  3pm3.2i  1259  eqssi  3652  elini  3830  dtru  4887  opnzi  4972  so0  5097  we0  5138  difxp  5593  ord0  5815  dfiota4  5917  funi  5958  funcnvsn  5974  fnresi  6046  fn0  6049  f0  6124  fconst  6129  f10  6207  f1o0  6211  f1oi  6212  f1osn  6214  isoid  6619  porpss  6983  ordon  7024  omssnlim  7121  fo1st  7230  fo2nd  7231  wfrfun  7470  wfr1  7478  iordsmo  7499  tfrlem7  7524  tfr1  7538  frfnom  7575  seqomlem2  7591  oawordeulem  7679  mapsnf1o2  7947  canth2  8154  unfilem2  8266  cantnfvalf  8600  cnfcom3clem  8640  tc2  8656  r111  8676  rankf  8695  cardf2  8807  harcard  8842  r0weon  8873  infxpenc  8879  infxpenc2lem1  8880  alephon  8930  alephf1  8946  alephiso  8959  alephsmo  8963  alephf1ALT  8964  alephfplem4  8968  ackbij1lem17  9096  ackbij1  9098  ackbij2  9103  isfin1-3  9246  fin1a2lem2  9261  fin1a2lem4  9263  axcc2lem  9296  iunfo  9399  smobeth  9446  0tsk  9615  1pi  9743  nqerf  9790  axaddf  10004  axmulf  10005  axicn  10009  mulnzcnopr  10711  negiso  11041  dfnn2  11071  nnind  11076  0z  11426  dfuzi  11506  cnref1o  11865  elrpii  11873  0e0icopnf  12320  0e0iccpnf  12321  fz0to4untppr  12481  fldiv4p1lem1div2  12676  om2uzf1oi  12792  om2uzisoi  12793  uzrdgfni  12797  expcl2lem  12912  expclzlem  12924  expge0  12936  expge1  12937  faclbnd4lem1  13120  hashkf  13159  wwlktovf1  13746  sqrtf  14147  fclim  14328  eff2  14873  reeff1  14894  ef01bndlem  14958  sin01bnd  14959  cos01bnd  14960  sin01gt0  14964  egt2lt3  14978  qnnen  14986  ruc  15016  halfleoddlt  15133  divalglem2  15165  divalglem9  15171  bitsf1  15215  sadaddlem  15235  2prm  15452  3prm  15453  1arith  15678  prmlem1a  15860  setsnid  15962  xpsff1o  16275  dmaf  16746  cdaf  16747  coapm  16768  isdrs2  16986  0pos  17001  isposi  17003  fpwipodrs  17211  letsr  17274  sgrp0b  17339  frmdplusg  17438  symg2bas  17864  pmtrsn  17985  odf  18002  efgsfo  18198  efgrelexlemb  18209  isabli  18253  mgpf  18605  prdscrngd  18659  xrsmgmdifsgrp  19831  xrs1cmn  19834  cnmgpid  19856  zringnzr  19878  zringunit  19884  zringlpir  19885  zringndrg  19886  zzngim  19949  cnmsgngrp  19973  psgninv  19976  zrhpsgnmhm  19978  retos  20012  refld  20013  pjpm  20100  fntopon  20776  istpsi  20794  0cmp  21245  cmpfi  21259  indisconn  21269  comppfsc  21383  kqf  21598  ptcmpfi  21664  fbssfi  21688  zfbas  21747  alexsubALTlem2  21899  alexsubALTlem4  21901  ptcmplem2  21904  ptcmp  21909  prdstmdd  21974  tsmsfbas  21978  ismeti  22177  prdsxmslem2  22381  cnfldms  22626  cnnrg  22631  tgqioo  22650  xrtgioo  22656  recld2  22664  xrge0gsumle  22683  xrge0tsms  22684  addcnlem  22714  divcn  22718  abscncf  22751  recncf  22752  imcncf  22753  cjcncf  22754  icopnfhmeo  22789  xrhmeo  22792  cnllycmp  22802  isclmi0  22944  iscvsi  22975  cnstrcvs  22987  cncvs  22991  cncms  23197  ovolf  23296  ovolicc1  23330  ovolre  23339  ioorf  23387  opnmblALT  23417  dveflem  23787  mdegxrf  23873  iaa  24125  ulmdm  24192  dvradcnv  24220  reeff1o  24246  reefiso  24247  reefgim  24249  recosf1o  24326  efifo  24338  rzgrp  24345  logcn  24438  cxpcn3  24534  resqrtcn  24535  logb1  24552  logbmpt  24571  ressatans  24706  lgamcvg2  24826  lgam1  24835  gam1  24836  efnnfsumcl  24874  efchtdvds  24930  ppiub  24974  lgslem2  25068  lgsfcl2  25073  lgsne0  25105  2lgslem1b  25162  padicabvf  25365  istrkg3ld  25405  axlowdimlem16  25882  upgrbi  26033  umgrbi  26041  lfuhgr1v0e  26191  cusgr0  26378  wlk2v2elem2  27134  upgr4cycl4dv4e  27163  konigsberglem4  27233  frgr0  27244  ex-pss  27415  ex-fl  27434  isgrpoi  27480  grporn  27503  isabloi  27533  smcnlem  27680  lnocoi  27740  cncph  27802  cnbn  27853  cnchl  27900  norm3adifii  28133  hhph  28163  hhhl  28189  hlim0  28220  hlimf  28222  helch  28228  hsn0elch  28233  hhssabloilem  28246  hhssnv  28249  hhshsslem2  28253  hhssbn  28265  hhsshl  28266  shscli  28304  shintcli  28316  chintcli  28318  shsval2i  28374  pjhthlem2  28379  lejdii  28525  nonbooli  28638  pjrni  28689  pjfoi  28690  pjfi  28691  pjmf1  28703  df0op2  28739  idunop  28965  0cnop  28966  0cnfn  28967  idcnop  28968  idhmop  28969  0hmop  28970  0lnfn  28972  0bdop  28980  lnophsi  28988  lnopcoi  28990  lnopunii  28999  lnophmi  29005  nmcopex  29016  nmcoplb  29017  nmcfnex  29040  nmcfnlb  29041  imaelshi  29045  nlelshi  29047  nlelchi  29048  riesz4i  29050  riesz4  29051  riesz1  29052  cnlnadjlem6  29059  cnlnadjlem9  29062  cnlnadjeui  29064  cnlnadjeu  29065  nmopadji  29077  bdophsi  29083  bdopcoi  29085  nmopcoadji  29088  pjhmopi  29133  pjbdlni  29136  hmopidmchi  29138  mdslj1i  29306  rinvf1o  29560  nnindf  29693  rpdp2cl  29717  dp2ltc  29722  dpmul4  29750  xrstos  29807  xrsclat  29808  xrge0omnd  29839  xrge0tsmsd  29913  reofld  29968  nn0archi  29971  xrge0iifmhm  30113  xrge0pluscn  30114  cnzh  30142  rezh  30143  qqhval2lem  30153  esum0  30239  esumcst  30253  esumpcvgval  30268  esumcvg  30276  dmvlsiga  30320  measdivcstOLD  30415  eulerpartlemt  30561  coinfliprv  30672  ballotlem2  30678  signswmnd  30762  logdivsqrle  30856  hgt750lem  30857  bnj906  31126  indispconn  31342  cnllysconn  31353  rellysconn  31359  msrf  31565  soseq  31879  frrlem5c  31911  bdayfo  31953  scutf  32044  brbigcup  32130  fobigcup  32132  brsingle  32149  fnsingle  32151  brimage  32158  funimage  32160  fnimage  32161  imageval  32162  brcart  32164  brapply  32170  brcup  32171  brcap  32172  funpartfun  32175  brub  32186  onsucconni  32561  onsucsuccmpi  32567  dnicn  32607  bj-dtru  32922  bj-rabtr  33051  bj-rabtrALTALT  33053  taupilem2  33298  taupi  33299  f1omptsnlem  33313  icoreresf  33330  relowlpssretop  33342  finxpreclem3  33360  matunitlindf  33537  mblfinlem2  33577  areacirc  33635  0totbnd  33702  heiborlem6  33745  refrelid  34411  isolatiN  34821  isomliN  34844  ishlatiN  34960  mzpclall  37607  jm2.20nn  37881  dfacbasgrp  37995  dgraaf  38034  ifpim3  38158  ifpim4  38160  ifpbi1b  38165  iso0  38823  dvsid  38847  halffl  39824  resincncf  40406  0cnf  40408  iblempty  40499  dirkeritg  40637  fourierdlem62  40703  fourierdlem76  40717  fourierdlem103  40744  etransclem18  40787  etransclem46  40815  abnotbtaxb  41403  fmtnof1  41772  fmtno4prm  41812  prmdvdsfmtnof1  41824  31prm  41837  0evenALTV  41924  1oddALTV  41926  2evenALTV  41928  6even  41945  8even  41947  6gbe  41984  7gbow  41985  8gbe  41986  9gbo  41987  11gbo  41988  sprsymrelf1  42071  uspgrsprf1  42080  1odd  42136  nnsgrp  42142  0even  42256  2even  42258  2zrngamgm  42264  2zrngasgrp  42265  2zrngamnd  42266  2zrngagrp  42268  2zrngmsgrp  42272  zlmodzxzldeplem3  42616  lvecpsslmod  42621  ldepsnlinc  42622  blennngt2o2  42711  blennn0e2  42713  setrec2lem2  42766  aacllem  42875
  Copyright terms: Public domain W3C validator