Theorem mpbir2and 944

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:  nnnninfeq2  7129  nqnq0pi  7439  genpassg  7527  addnqpr  7562  mulnqpr  7578  distrprg  7589  1idpr  7593  ltexpri  7614  recexprlemex  7638  aptipr  7642  cauappcvgprlemladd  7659  ltntri  8087  add20  8433  inelr  8543  recgt0  8809  prodgt0  8811  squeeze0  8863  suprzclex  9353  eluzadd  9558  eluzsub  9559  xrletrid  9807  xrre  9822  xrre3  9824  xleadd1a  9875  elioc2  9938  elico2  9939  elicc2  9940  elfz1eq  10037  fztri3or  10041  fznatpl1  10078  nn0fz0  10121  fzctr  10135  fzo1fzo0n0  10185  fzoaddel  10194  exbtwnz  10253  flid  10286  flqaddz  10299  flqdiv  10323  modqid  10351  frec2uzf1od  10408  iseqf1olemqk  10496  bcval5  10745  abs2difabs  11119  fzomaxdiflem  11123  icodiamlt  11191  dfabsmax  11228  rexico  11232  mul0inf  11251  xrbdtri  11286  sumeq2  11369  sumsnf  11419  fsum00  11472  prodeq2  11567  prodsnf  11602  zsupcllemstep  11948  zssinfcl  11951  gcd0id  11982  gcdneg  11985  nn0seqcvgd  12043  lcmval  12065  lcmneg  12076  qredeq  12098  prmind2  12122  pw2dvdseu  12170  hashdvds  12223  pcpremul  12295  pcidlem  12324  pcgcd1  12329  fldivp1  12348  pcfaclem  12349  ennnfonelemex  12417  ennnfonelemnn0  12425  mnd1  12852  grp1  12981  0subg  13064  nmznsg  13078  ring1  13241  dvdsrmuld  13270  1unit  13281  unitmulcl  13287  unitgrp  13290  unitnegcl  13304  subrguss  13362  subrgunit  13365  lsslsp  13520  tgcl  13649  distop  13670  epttop  13675  neiss  13735  opnneissb  13740  ssnei2  13742  innei  13748  lmconst  13801  cnpnei  13804  cnptopco  13807  cnss1  13811  cnss2  13812  cncnpi  13813  cncnp  13815  cnconst2  13818  cnrest  13820  cnptopresti  13823  cnpdis  13827  lmtopcnp  13835  neitx  13853  tx1cn  13854  tx2cn  13855  txcnp  13856  txcnmpt  13858  txdis1cn  13863  psmetsym  13914  psmetres2  13918  isxmetd  13932  xmetsym  13953  xmetpsmet  13954  metrtri  13962  xblss2ps  13989  xblss2  13990  xblcntrps  13998  xblcntr  13999  bdxmet  14086  bdmet  14087  bdmopn  14089  xmetxp  14092  xmetxpbl  14093  rescncf  14153  cncfco  14163  mulcncflem  14175  mulcncf  14176  suplociccreex  14187  ivthinclemlopn  14199  ivthinclemuopn  14201  cnplimcim  14221  cnplimclemr  14223  limccnpcntop  14229  limccnp2cntop  14231  limccoap  14232  dvidlemap  14245  dvcn  14249  dvaddxxbr  14250  dvmulxxbr  14251  dvcoapbr  14256  dvcjbr  14257  dvrecap  14262  rpabscxpbnd  14444  lgsdirprm  14520  lgseisenlem1  14535  lgseisenlem2  14536  2sqlem8  14555  refeq  14861  apdifflemf  14879  ltlenmkv  14903