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  7296  nnnninfeq2  7476  nqnq0pi  7812  genpassg  7900  addnqpr  7935  mulnqpr  7951  distrprg  7962  1idpr  7966  ltexpri  7987  recexprlemex  8011  aptipr  8015  cauappcvgprlemladd  8032  letrid  8450  ltntri  8462  add20  8810  inelr  8921  recgt0  9189  prodgt0  9191  squeeze0  9243  suprzclex  9756  eluzadd  9968  eluzsub  9969  xrletrid  10225  xrre  10240  xrre3  10242  xleadd1a  10293  elioc2  10356  elico2  10357  elicc2  10358  elfz1eq  10457  fztri3or  10461  fzspl  10494  fznatpl1  10501  nn0fz0  10544  fzctr  10558  fzo1fzo0n0  10613  fzoaddel  10623  elincfzoext  10629  zsupcllemstep  10680  zssinfcl  10683  exbtwnz  10703  flid  10741  flqaddz  10754  flqdiv  10780  modqid  10808  frec2uzf1od  10865  iseqf1olemqk  10966  bcval5  11224  hashf1lem1  11308  eqs1  11419  pfxccatin12d  11540  abs2difabs  11898  fzomaxdiflem  11902  icodiamlt  11970  dfabsmax  12007  rexico  12011  mul0inf  12033  xrbdtri  12068  sumeq2  12151  sumsnf  12202  fsum00  12255  prodeq2  12350  prodsnf  12385  bitsfzolem  12747  bitsfzo  12748  bitsmod  12749  bitscmp  12751  gcd0id  12782  gcdneg  12785  nn0seqcvgd  12845  lcmval  12867  lcmneg  12878  qredeq  12900  prmind2  12924  pcpremul  13102  pcidlem  13132  pcgcd1  13137  fldivp1  13157  pcfaclem  13158  4sqlem17  13216  ballotfilemfc0  13291  ballotfilemfcc  13292  ennnfonelemex  13364  ennnfonelemnn0  13372  mnd1  13822  grp1  13971  0subg  14062  nmznsg  14076  ghmpreima  14129  ghmeql  14130  ghmnsgpreima  14132  kerf1ghm  14137  cntzsgrpcl  14168  cntzsubm  14171  cntzsubg  14172  cntzmhm  14174  ring1  14472  dvdsrmuld  14513  1unit  14524  unitmulcl  14530  unitgrp  14533  unitnegcl  14547  rhmdvdsr  14592  elrhmunit  14594  subrngintm  14630  subrguss  14654  subrgunit  14657  rhmeql  14668  rhmima  14669  lsslsp  14876  rnglidlrng  14945  issubassa  15123  issubassa2  15145  fczpsrbag  15171  psrbaglecl  15174  psrbagcon  15176  mplsubgfilemm  15226  mplsubgfilemcl  15227  mplsubgfileminv  15228  tgcl  15302  distop  15323  epttop  15328  neiss  15388  opnneissb  15393  ssnei2  15395  innei  15401  lmconst  15454  cnpnei  15457  cnptopco  15460  cnss1  15464  cnss2  15465  cncnpi  15466  cncnp  15468  cnconst2  15471  cnrest  15473  cnptopresti  15476  cnpdis  15480  lmtopcnp  15488  neitx  15506  tx1cn  15507  tx2cn  15508  txcnp  15509  txcnmpt  15511  txdis1cn  15516  psmetsym  15567  psmetres2  15571  isxmetd  15585  xmetsym  15606  xmetpsmet  15607  metrtri  15615  xblss2ps  15642  xblss2  15643  xblcntrps  15651  xblcntr  15652  bdxmet  15739  bdmet  15740  bdmopn  15742  xmetxp  15745  xmetxpbl  15746  rescncf  15819  cncfco  15829  mulcncflem  15845  mulcncf  15846  suplociccreex  15862  ivthinclemlopn  15874  ivthinclemuopn  15876  hovera  15885  hoverlt1  15887  cnplimcim  15905  cnplimclemr  15907  limccnpcntop  15913  limccnp2cntop  15915  limccoap  15916  dvidlemap  15929  dvidrelem  15930  dvidsslem  15931  dvcn  15938  dvaddxxbr  15939  dvmulxxbr  15940  dvcoapbr  15945  dvcjbr  15946  dvrecap  15951  rpabscxpbnd  16187  dvdsppwf1o  16295  chtqub  16308  bposlem1  16323  bposlem2  16324  lgsdirprm  16370  lgseisenlem1  16406  lgseisenlem2  16407  lgseisenlem3  16408  lgsquadlem1  16413  2sqlem8  16459  uspgr2wlkeq2  16824  clwwlknccat  16881  clwwlknonex2lem2  16896  eupthres  16915  refeq  17291  apdifflemf  17314  ltlenmkv  17339