Theorem mpbir2and 946

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  7204  nqnq0pi  7524  genpassg  7612  addnqpr  7647  mulnqpr  7663  distrprg  7674  1idpr  7678  ltexpri  7699  recexprlemex  7723  aptipr  7727  cauappcvgprlemladd  7744  ltntri  8173  add20  8520  inelr  8630  recgt0  8896  prodgt0  8898  squeeze0  8950  suprzclex  9443  eluzadd  9649  eluzsub  9650  xrletrid  9899  xrre  9914  xrre3  9916  xleadd1a  9967  elioc2  10030  elico2  10031  elicc2  10032  elfz1eq  10129  fztri3or  10133  fznatpl1  10170  nn0fz0  10213  fzctr  10227  fzo1fzo0n0  10278  fzoaddel  10287  zsupcllemstep  10338  zssinfcl  10341  exbtwnz  10359  flid  10393  flqaddz  10406  flqdiv  10432  modqid  10460  frec2uzf1od  10517  iseqf1olemqk  10618  bcval5  10874  abs2difabs  11292  fzomaxdiflem  11296  icodiamlt  11364  dfabsmax  11401  rexico  11405  mul0inf  11425  xrbdtri  11460  sumeq2  11543  sumsnf  11593  fsum00  11646  prodeq2  11741  prodsnf  11776  bitsfzolem  12138  bitsfzo  12139  bitsmod  12140  bitscmp  12142  gcd0id  12173  gcdneg  12176  nn0seqcvgd  12236  lcmval  12258  lcmneg  12269  qredeq  12291  prmind2  12315  pw2dvdseu  12363  hashdvds  12416  pcpremul  12489  pcidlem  12519  pcgcd1  12524  fldivp1  12544  pcfaclem  12545  4sqlem17  12603  ennnfonelemex  12658  ennnfonelemnn0  12666  mnd1  13159  grp1  13310  0subg  13407  nmznsg  13421  ghmpreima  13474  ghmeql  13475  ghmnsgpreima  13477  kerf1ghm  13482  ring1  13693  dvdsrmuld  13730  1unit  13741  unitmulcl  13747  unitgrp  13750  unitnegcl  13764  rhmdvdsr  13809  elrhmunit  13811  subrngintm  13846  subrguss  13870  subrgunit  13873  rhmeql  13884  rhmima  13885  lsslsp  14063  rnglidlrng  14132  fczpsrbag  14305  mplsubgfilemm  14332  mplsubgfilemcl  14333  mplsubgfileminv  14334  tgcl  14408  distop  14429  epttop  14434  neiss  14494  opnneissb  14499  ssnei2  14501  innei  14507  lmconst  14560  cnpnei  14563  cnptopco  14566  cnss1  14570  cnss2  14571  cncnpi  14572  cncnp  14574  cnconst2  14577  cnrest  14579  cnptopresti  14582  cnpdis  14586  lmtopcnp  14594  neitx  14612  tx1cn  14613  tx2cn  14614  txcnp  14615  txcnmpt  14617  txdis1cn  14622  psmetsym  14673  psmetres2  14677  isxmetd  14691  xmetsym  14712  xmetpsmet  14713  metrtri  14721  xblss2ps  14748  xblss2  14749  xblcntrps  14757  xblcntr  14758  bdxmet  14845  bdmet  14846  bdmopn  14848  xmetxp  14851  xmetxpbl  14852  rescncf  14925  cncfco  14935  mulcncflem  14951  mulcncf  14952  suplociccreex  14968  ivthinclemlopn  14980  ivthinclemuopn  14982  hovera  14991  hoverlt1  14993  cnplimcim  15011  cnplimclemr  15013  limccnpcntop  15019  limccnp2cntop  15021  limccoap  15022  dvidlemap  15035  dvidrelem  15036  dvidsslem  15037  dvcn  15044  dvaddxxbr  15045  dvmulxxbr  15046  dvcoapbr  15051  dvcjbr  15052  dvrecap  15057  rpabscxpbnd  15284  dvdsppwf1o  15333  lgsdirprm  15383  lgseisenlem1  15419  lgseisenlem2  15420  lgseisenlem3  15421  lgsquadlem1  15426  2sqlem8  15472  refeq  15785  apdifflemf  15803  ltlenmkv  15827