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  3774  nnnninfeq2  7304  nqnq0pi  7633  genpassg  7721  addnqpr  7756  mulnqpr  7772  distrprg  7783  1idpr  7787  ltexpri  7808  recexprlemex  7832  aptipr  7836  cauappcvgprlemladd  7853  ltntri  8282  add20  8629  inelr  8739  recgt0  9005  prodgt0  9007  squeeze0  9059  suprzclex  9553  eluzadd  9759  eluzsub  9760  xrletrid  10009  xrre  10024  xrre3  10026  xleadd1a  10077  elioc2  10140  elico2  10141  elicc2  10142  elfz1eq  10239  fztri3or  10243  fznatpl1  10280  nn0fz0  10323  fzctr  10337  fzo1fzo0n0  10391  fzoaddel  10401  elincfzoext  10407  zsupcllemstep  10457  zssinfcl  10460  exbtwnz  10478  flid  10512  flqaddz  10525  flqdiv  10551  modqid  10579  frec2uzf1od  10636  iseqf1olemqk  10737  bcval5  10993  eqs1  11169  pfxccatin12d  11285  abs2difabs  11627  fzomaxdiflem  11631  icodiamlt  11699  dfabsmax  11736  rexico  11740  mul0inf  11760  xrbdtri  11795  sumeq2  11878  sumsnf  11928  fsum00  11981  prodeq2  12076  prodsnf  12111  bitsfzolem  12473  bitsfzo  12474  bitsmod  12475  bitscmp  12477  gcd0id  12508  gcdneg  12511  nn0seqcvgd  12571  lcmval  12593  lcmneg  12604  qredeq  12626  prmind2  12650  pw2dvdseu  12698  hashdvds  12751  pcpremul  12824  pcidlem  12854  pcgcd1  12859  fldivp1  12879  pcfaclem  12880  4sqlem17  12938  ennnfonelemex  12993  ennnfonelemnn0  13001  mnd1  13496  grp1  13647  0subg  13744  nmznsg  13758  ghmpreima  13811  ghmeql  13812  ghmnsgpreima  13814  kerf1ghm  13819  ring1  14030  dvdsrmuld  14068  1unit  14079  unitmulcl  14085  unitgrp  14088  unitnegcl  14102  rhmdvdsr  14147  elrhmunit  14149  subrngintm  14184  subrguss  14208  subrgunit  14211  rhmeql  14222  rhmima  14223  lsslsp  14401  rnglidlrng  14470  fczpsrbag  14643  mplsubgfilemm  14670  mplsubgfilemcl  14671  mplsubgfileminv  14672  tgcl  14746  distop  14767  epttop  14772  neiss  14832  opnneissb  14837  ssnei2  14839  innei  14845  lmconst  14898  cnpnei  14901  cnptopco  14904  cnss1  14908  cnss2  14909  cncnpi  14910  cncnp  14912  cnconst2  14915  cnrest  14917  cnptopresti  14920  cnpdis  14924  lmtopcnp  14932  neitx  14950  tx1cn  14951  tx2cn  14952  txcnp  14953  txcnmpt  14955  txdis1cn  14960  psmetsym  15011  psmetres2  15015  isxmetd  15029  xmetsym  15050  xmetpsmet  15051  metrtri  15059  xblss2ps  15086  xblss2  15087  xblcntrps  15095  xblcntr  15096  bdxmet  15183  bdmet  15184  bdmopn  15186  xmetxp  15189  xmetxpbl  15190  rescncf  15263  cncfco  15273  mulcncflem  15289  mulcncf  15290  suplociccreex  15306  ivthinclemlopn  15318  ivthinclemuopn  15320  hovera  15329  hoverlt1  15331  cnplimcim  15349  cnplimclemr  15351  limccnpcntop  15357  limccnp2cntop  15359  limccoap  15360  dvidlemap  15373  dvidrelem  15374  dvidsslem  15375  dvcn  15382  dvaddxxbr  15383  dvmulxxbr  15384  dvcoapbr  15389  dvcjbr  15390  dvrecap  15395  rpabscxpbnd  15622  dvdsppwf1o  15671  lgsdirprm  15721  lgseisenlem1  15757  lgseisenlem2  15758  lgseisenlem3  15759  lgsquadlem1  15764  2sqlem8  15810  uspgr2wlkeq2  16087  refeq  16426  apdifflemf  16444  ltlenmkv  16468