Theorem mpbir2and 957

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 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  ifpprsnssdc  3820  isfsuppd  7290  nnnninfeq2  7470  nqnq0pi  7806  genpassg  7894  addnqpr  7929  mulnqpr  7945  distrprg  7956  1idpr  7960  ltexpri  7981  recexprlemex  8005  aptipr  8009  cauappcvgprlemladd  8026  letrid  8444  ltntri  8456  add20  8804  inelr  8915  recgt0  9183  prodgt0  9185  squeeze0  9237  suprzclex  9749  eluzadd  9961  eluzsub  9962  xrletrid  10218  xrre  10233  xrre3  10235  xleadd1a  10286  elioc2  10349  elico2  10350  elicc2  10351  elfz1eq  10450  fztri3or  10454  fzspl  10487  fznatpl1  10494  nn0fz0  10537  fzctr  10551  fzo1fzo0n0  10606  fzoaddel  10616  elincfzoext  10622  zsupcllemstep  10673  zssinfcl  10676  exbtwnz  10696  flid  10734  flqaddz  10747  flqdiv  10773  modqid  10801  frec2uzf1od  10858  iseqf1olemqk  10959  bcval5  11217  hashf1lem1  11301  eqs1  11412  pfxccatin12d  11533  abs2difabs  11891  fzomaxdiflem  11895  icodiamlt  11963  dfabsmax  12000  rexico  12004  mul0inf  12026  xrbdtri  12061  sumeq2  12144  sumsnf  12195  fsum00  12248  prodeq2  12343  prodsnf  12378  bitsfzolem  12740  bitsfzo  12741  bitsmod  12742  bitscmp  12744  gcd0id  12775  gcdneg  12778  nn0seqcvgd  12838  lcmval  12860  lcmneg  12871  qredeq  12893  prmind2  12917  pcpremul  13095  pcidlem  13125  pcgcd1  13130  fldivp1  13150  pcfaclem  13151  4sqlem17  13209  ballotfilemfc0  13284  ballotfilemfcc  13285  ennnfonelemex  13357  ennnfonelemnn0  13365  mnd1  13815  grp1  13964  0subg  14055  nmznsg  14069  ghmpreima  14122  ghmeql  14123  ghmnsgpreima  14125  kerf1ghm  14130  cntzsgrpcl  14161  cntzsubm  14164  cntzsubg  14165  cntzmhm  14167  ring1  14448  dvdsrmuld  14487  1unit  14498  unitmulcl  14504  unitgrp  14507  unitnegcl  14521  rhmdvdsr  14566  elrhmunit  14568  subrngintm  14604  subrguss  14628  subrgunit  14631  rhmeql  14642  rhmima  14643  lsslsp  14850  rnglidlrng  14919  issubassa  15097  issubassa2  15119  fczpsrbag  15140  psrbaglecl  15144  psrbagcon  15146  mplsubgfilemm  15180  mplsubgfilemcl  15181  mplsubgfileminv  15182  tgcl  15256  distop  15277  epttop  15282  neiss  15342  opnneissb  15347  ssnei2  15349  innei  15355  lmconst  15408  cnpnei  15411  cnptopco  15414  cnss1  15418  cnss2  15419  cncnpi  15420  cncnp  15422  cnconst2  15425  cnrest  15427  cnptopresti  15430  cnpdis  15434  lmtopcnp  15442  neitx  15460  tx1cn  15461  tx2cn  15462  txcnp  15463  txcnmpt  15465  txdis1cn  15470  psmetsym  15521  psmetres2  15525  isxmetd  15539  xmetsym  15560  xmetpsmet  15561  metrtri  15569  xblss2ps  15596  xblss2  15597  xblcntrps  15605  xblcntr  15606  bdxmet  15693  bdmet  15694  bdmopn  15696  xmetxp  15699  xmetxpbl  15700  rescncf  15773  cncfco  15783  mulcncflem  15799  mulcncf  15800  suplociccreex  15816  ivthinclemlopn  15828  ivthinclemuopn  15830  hovera  15839  hoverlt1  15841  cnplimcim  15859  cnplimclemr  15861  limccnpcntop  15867  limccnp2cntop  15869  limccoap  15870  dvidlemap  15883  dvidrelem  15884  dvidsslem  15885  dvcn  15892  dvaddxxbr  15893  dvmulxxbr  15894  dvcoapbr  15899  dvcjbr  15900  dvrecap  15905  rpabscxpbnd  16141  dvdsppwf1o  16249  chtqub  16262  bposlem1  16277  bposlem2  16278  lgsdirprm  16324  lgseisenlem1  16360  lgseisenlem2  16361  lgseisenlem3  16362  lgsquadlem1  16367  2sqlem8  16413  uspgr2wlkeq2  16778  clwwlknccat  16835  clwwlknonex2lem2  16850  eupthres  16869  refeq  17244  apdifflemf  17267  ltlenmkv  17292