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  14303  tgcl  14386  distop  14407  epttop  14412  neiss  14472  opnneissb  14477  ssnei2  14479  innei  14485  lmconst  14538  cnpnei  14541  cnptopco  14544  cnss1  14548  cnss2  14549  cncnpi  14550  cncnp  14552  cnconst2  14555  cnrest  14557  cnptopresti  14560  cnpdis  14564  lmtopcnp  14572  neitx  14590  tx1cn  14591  tx2cn  14592  txcnp  14593  txcnmpt  14595  txdis1cn  14600  psmetsym  14651  psmetres2  14655  isxmetd  14669  xmetsym  14690  xmetpsmet  14691  metrtri  14699  xblss2ps  14726  xblss2  14727  xblcntrps  14735  xblcntr  14736  bdxmet  14823  bdmet  14824  bdmopn  14826  xmetxp  14829  xmetxpbl  14830  rescncf  14903  cncfco  14913  mulcncflem  14929  mulcncf  14930  suplociccreex  14946  ivthinclemlopn  14958  ivthinclemuopn  14960  hovera  14969  hoverlt1  14971  cnplimcim  14989  cnplimclemr  14991  limccnpcntop  14997  limccnp2cntop  14999  limccoap  15000  dvidlemap  15013  dvidrelem  15014  dvidsslem  15015  dvcn  15022  dvaddxxbr  15023  dvmulxxbr  15024  dvcoapbr  15029  dvcjbr  15030  dvrecap  15035  rpabscxpbnd  15262  dvdsppwf1o  15311  lgsdirprm  15361  lgseisenlem1  15397  lgseisenlem2  15398  lgseisenlem3  15399  lgsquadlem1  15404  2sqlem8  15450  refeq  15763  apdifflemf  15781  ltlenmkv  15805