Theorem mpbir2and 953

Description: Detach a conjunction of truths in a biconditional. (Contributed by NM, 6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Hypotheses

Ref	Expression
mpbir2and.1	⊢ (𝜑 → 𝜒)
mpbir2and.2	⊢ (𝜑 → 𝜃)
mpbir2and.3	⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))

Assertion

Ref	Expression
mpbir2and	⊢ (𝜑 → 𝜓)

Proof of Theorem mpbir2and

Step	Hyp	Ref	Expression
1		mpbir2and.1	. . 3 ⊢ (𝜑 → 𝜒)
2		mpbir2and.2	. . 3 ⊢ (𝜑 → 𝜃)
3	1, 2	jca 306	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
4		mpbir2and.3	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))
5	3, 4	mpbird 167	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ifpprsnssdc  3801  isfsuppd  7245  nnnninfeq2  7422  nqnq0pi  7758  genpassg  7846  addnqpr  7881  mulnqpr  7897  distrprg  7908  1idpr  7912  ltexpri  7933  recexprlemex  7957  aptipr  7961  cauappcvgprlemladd  7978  ltntri  8406  add20  8753  inelr  8863  recgt0  9129  prodgt0  9131  squeeze0  9183  suprzclex  9682  eluzadd  9889  eluzsub  9890  xrletrid  10144  xrre  10159  xrre3  10161  xleadd1a  10212  elioc2  10275  elico2  10276  elicc2  10277  elfz1eq  10375  fztri3or  10379  fzspl  10410  fznatpl1  10417  nn0fz0  10460  fzctr  10474  fzo1fzo0n0  10529  fzoaddel  10539  elincfzoext  10545  zsupcllemstep  10596  zssinfcl  10599  exbtwnz  10617  flid  10651  flqaddz  10664  flqdiv  10690  modqid  10718  frec2uzf1od  10775  iseqf1olemqk  10876  bcval5  11133  eqs1  11324  pfxccatin12d  11445  abs2difabs  11801  fzomaxdiflem  11805  icodiamlt  11873  dfabsmax  11910  rexico  11914  mul0inf  11934  xrbdtri  11969  sumeq2  12052  sumsnf  12103  fsum00  12156  prodeq2  12251  prodsnf  12286  bitsfzolem  12648  bitsfzo  12649  bitsmod  12650  bitscmp  12652  gcd0id  12683  gcdneg  12686  nn0seqcvgd  12746  lcmval  12768  lcmneg  12779  qredeq  12801  prmind2  12825  pw2dvdseu  12873  pcpremul  12999  pcidlem  13029  pcgcd1  13034  fldivp1  13054  pcfaclem  13055  4sqlem17  13113  ballotfilemfc0  13157  ballotfilemfcc  13158  ennnfonelemex  13186  ennnfonelemnn0  13194  mnd1  13689  grp1  13840  0subg  13937  nmznsg  13951  ghmpreima  14004  ghmeql  14005  ghmnsgpreima  14007  kerf1ghm  14012  ring1  14224  dvdsrmuld  14263  1unit  14274  unitmulcl  14280  unitgrp  14283  unitnegcl  14297  rhmdvdsr  14342  elrhmunit  14344  subrngintm  14380  subrguss  14404  subrgunit  14407  rhmeql  14418  rhmima  14419  lsslsp  14626  rnglidlrng  14695  fczpsrbag  14869  psrbaglecl  14873  psrbagcon  14875  mplsubgfilemm  14902  mplsubgfilemcl  14903  mplsubgfileminv  14904  tgcl  14978  distop  14999  epttop  15004  neiss  15064  opnneissb  15069  ssnei2  15071  innei  15077  lmconst  15130  cnpnei  15133  cnptopco  15136  cnss1  15140  cnss2  15141  cncnpi  15142  cncnp  15144  cnconst2  15147  cnrest  15149  cnptopresti  15152  cnpdis  15156  lmtopcnp  15164  neitx  15182  tx1cn  15183  tx2cn  15184  txcnp  15185  txcnmpt  15187  txdis1cn  15192  psmetsym  15243  psmetres2  15247  isxmetd  15261  xmetsym  15282  xmetpsmet  15283  metrtri  15291  xblss2ps  15318  xblss2  15319  xblcntrps  15327  xblcntr  15328  bdxmet  15415  bdmet  15416  bdmopn  15418  xmetxp  15421  xmetxpbl  15422  rescncf  15495  cncfco  15505  mulcncflem  15521  mulcncf  15522  suplociccreex  15538  ivthinclemlopn  15550  ivthinclemuopn  15552  hovera  15561  hoverlt1  15563  cnplimcim  15581  cnplimclemr  15583  limccnpcntop  15589  limccnp2cntop  15591  limccoap  15592  dvidlemap  15605  dvidrelem  15606  dvidsslem  15607  dvcn  15614  dvaddxxbr  15615  dvmulxxbr  15616  dvcoapbr  15621  dvcjbr  15622  dvrecap  15627  rpabscxpbnd  15854  dvdsppwf1o  15906  lgsdirprm  15956  lgseisenlem1  15992  lgseisenlem2  15993  lgseisenlem3  15994  lgsquadlem1  15999  2sqlem8  16045  uspgr2wlkeq2  16410  clwwlknccat  16467  clwwlknonex2lem2  16482  eupthres  16501  refeq  16857  apdifflemf  16879  ltlenmkv  16905