Theorem mpbir2and 950

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  3777  nnnninfeq2  7322  nqnq0pi  7651  genpassg  7739  addnqpr  7774  mulnqpr  7790  distrprg  7801  1idpr  7805  ltexpri  7826  recexprlemex  7850  aptipr  7854  cauappcvgprlemladd  7871  ltntri  8300  add20  8647  inelr  8757  recgt0  9023  prodgt0  9025  squeeze0  9077  suprzclex  9571  eluzadd  9778  eluzsub  9779  xrletrid  10033  xrre  10048  xrre3  10050  xleadd1a  10101  elioc2  10164  elico2  10165  elicc2  10166  elfz1eq  10263  fztri3or  10267  fznatpl1  10304  nn0fz0  10347  fzctr  10361  fzo1fzo0n0  10415  fzoaddel  10425  elincfzoext  10431  zsupcllemstep  10482  zssinfcl  10485  exbtwnz  10503  flid  10537  flqaddz  10550  flqdiv  10576  modqid  10604  frec2uzf1od  10661  iseqf1olemqk  10762  bcval5  11018  eqs1  11198  pfxccatin12d  11319  abs2difabs  11662  fzomaxdiflem  11666  icodiamlt  11734  dfabsmax  11771  rexico  11775  mul0inf  11795  xrbdtri  11830  sumeq2  11913  sumsnf  11963  fsum00  12016  prodeq2  12111  prodsnf  12146  bitsfzolem  12508  bitsfzo  12509  bitsmod  12510  bitscmp  12512  gcd0id  12543  gcdneg  12546  nn0seqcvgd  12606  lcmval  12628  lcmneg  12639  qredeq  12661  prmind2  12685  pw2dvdseu  12733  hashdvds  12786  pcpremul  12859  pcidlem  12889  pcgcd1  12894  fldivp1  12914  pcfaclem  12915  4sqlem17  12973  ennnfonelemex  13028  ennnfonelemnn0  13036  mnd1  13531  grp1  13682  0subg  13779  nmznsg  13793  ghmpreima  13846  ghmeql  13847  ghmnsgpreima  13849  kerf1ghm  13854  ring1  14065  dvdsrmuld  14103  1unit  14114  unitmulcl  14120  unitgrp  14123  unitnegcl  14137  rhmdvdsr  14182  elrhmunit  14184  subrngintm  14219  subrguss  14243  subrgunit  14246  rhmeql  14257  rhmima  14258  lsslsp  14436  rnglidlrng  14505  fczpsrbag  14678  mplsubgfilemm  14705  mplsubgfilemcl  14706  mplsubgfileminv  14707  tgcl  14781  distop  14802  epttop  14807  neiss  14867  opnneissb  14872  ssnei2  14874  innei  14880  lmconst  14933  cnpnei  14936  cnptopco  14939  cnss1  14943  cnss2  14944  cncnpi  14945  cncnp  14947  cnconst2  14950  cnrest  14952  cnptopresti  14955  cnpdis  14959  lmtopcnp  14967  neitx  14985  tx1cn  14986  tx2cn  14987  txcnp  14988  txcnmpt  14990  txdis1cn  14995  psmetsym  15046  psmetres2  15050  isxmetd  15064  xmetsym  15085  xmetpsmet  15086  metrtri  15094  xblss2ps  15121  xblss2  15122  xblcntrps  15130  xblcntr  15131  bdxmet  15218  bdmet  15219  bdmopn  15221  xmetxp  15224  xmetxpbl  15225  rescncf  15298  cncfco  15308  mulcncflem  15324  mulcncf  15325  suplociccreex  15341  ivthinclemlopn  15353  ivthinclemuopn  15355  hovera  15364  hoverlt1  15366  cnplimcim  15384  cnplimclemr  15386  limccnpcntop  15392  limccnp2cntop  15394  limccoap  15395  dvidlemap  15408  dvidrelem  15409  dvidsslem  15410  dvcn  15417  dvaddxxbr  15418  dvmulxxbr  15419  dvcoapbr  15424  dvcjbr  15425  dvrecap  15430  rpabscxpbnd  15657  dvdsppwf1o  15706  lgsdirprm  15756  lgseisenlem1  15792  lgseisenlem2  15793  lgseisenlem3  15794  lgsquadlem1  15799  2sqlem8  15845  uspgr2wlkeq2  16177  clwwlknccat  16232  clwwlknonex2lem2  16247  eupthres  16266  refeq  16582  apdifflemf  16600  ltlenmkv  16624