Theorem mpbir2and 947

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  7238  nqnq0pi  7558  genpassg  7646  addnqpr  7681  mulnqpr  7697  distrprg  7708  1idpr  7712  ltexpri  7733  recexprlemex  7757  aptipr  7761  cauappcvgprlemladd  7778  ltntri  8207  add20  8554  inelr  8664  recgt0  8930  prodgt0  8932  squeeze0  8984  suprzclex  9478  eluzadd  9684  eluzsub  9685  xrletrid  9934  xrre  9949  xrre3  9951  xleadd1a  10002  elioc2  10065  elico2  10066  elicc2  10067  elfz1eq  10164  fztri3or  10168  fznatpl1  10205  nn0fz0  10248  fzctr  10262  fzo1fzo0n0  10314  fzoaddel  10323  elincfzoext  10329  zsupcllemstep  10379  zssinfcl  10382  exbtwnz  10400  flid  10434  flqaddz  10447  flqdiv  10473  modqid  10501  frec2uzf1od  10558  iseqf1olemqk  10659  bcval5  10915  eqs1  11090  abs2difabs  11463  fzomaxdiflem  11467  icodiamlt  11535  dfabsmax  11572  rexico  11576  mul0inf  11596  xrbdtri  11631  sumeq2  11714  sumsnf  11764  fsum00  11817  prodeq2  11912  prodsnf  11947  bitsfzolem  12309  bitsfzo  12310  bitsmod  12311  bitscmp  12313  gcd0id  12344  gcdneg  12347  nn0seqcvgd  12407  lcmval  12429  lcmneg  12440  qredeq  12462  prmind2  12486  pw2dvdseu  12534  hashdvds  12587  pcpremul  12660  pcidlem  12690  pcgcd1  12695  fldivp1  12715  pcfaclem  12716  4sqlem17  12774  ennnfonelemex  12829  ennnfonelemnn0  12837  mnd1  13331  grp1  13482  0subg  13579  nmznsg  13593  ghmpreima  13646  ghmeql  13647  ghmnsgpreima  13649  kerf1ghm  13654  ring1  13865  dvdsrmuld  13902  1unit  13913  unitmulcl  13919  unitgrp  13922  unitnegcl  13936  rhmdvdsr  13981  elrhmunit  13983  subrngintm  14018  subrguss  14042  subrgunit  14045  rhmeql  14056  rhmima  14057  lsslsp  14235  rnglidlrng  14304  fczpsrbag  14477  mplsubgfilemm  14504  mplsubgfilemcl  14505  mplsubgfileminv  14506  tgcl  14580  distop  14601  epttop  14606  neiss  14666  opnneissb  14671  ssnei2  14673  innei  14679  lmconst  14732  cnpnei  14735  cnptopco  14738  cnss1  14742  cnss2  14743  cncnpi  14744  cncnp  14746  cnconst2  14749  cnrest  14751  cnptopresti  14754  cnpdis  14758  lmtopcnp  14766  neitx  14784  tx1cn  14785  tx2cn  14786  txcnp  14787  txcnmpt  14789  txdis1cn  14794  psmetsym  14845  psmetres2  14849  isxmetd  14863  xmetsym  14884  xmetpsmet  14885  metrtri  14893  xblss2ps  14920  xblss2  14921  xblcntrps  14929  xblcntr  14930  bdxmet  15017  bdmet  15018  bdmopn  15020  xmetxp  15023  xmetxpbl  15024  rescncf  15097  cncfco  15107  mulcncflem  15123  mulcncf  15124  suplociccreex  15140  ivthinclemlopn  15152  ivthinclemuopn  15154  hovera  15163  hoverlt1  15165  cnplimcim  15183  cnplimclemr  15185  limccnpcntop  15191  limccnp2cntop  15193  limccoap  15194  dvidlemap  15207  dvidrelem  15208  dvidsslem  15209  dvcn  15216  dvaddxxbr  15217  dvmulxxbr  15218  dvcoapbr  15223  dvcjbr  15224  dvrecap  15229  rpabscxpbnd  15456  dvdsppwf1o  15505  lgsdirprm  15555  lgseisenlem1  15591  lgseisenlem2  15592  lgseisenlem3  15593  lgsquadlem1  15598  2sqlem8  15644  refeq  16041  apdifflemf  16059  ltlenmkv  16083