Theorem mpbir2and 934

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 304	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
4		mpbir2and.3	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))
5	3, 4	mpbird 166	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  nnnninfeq2  7093  nqnq0pi  7379  genpassg  7467  addnqpr  7502  mulnqpr  7518  distrprg  7529  1idpr  7533  ltexpri  7554  recexprlemex  7578  aptipr  7582  cauappcvgprlemladd  7599  ltntri  8026  add20  8372  inelr  8482  recgt0  8745  prodgt0  8747  squeeze0  8799  suprzclex  9289  eluzadd  9494  eluzsub  9495  xrletrid  9741  xrre  9756  xrre3  9758  xleadd1a  9809  elioc2  9872  elico2  9873  elicc2  9874  elfz1eq  9970  fztri3or  9974  fznatpl1  10011  nn0fz0  10054  fzctr  10068  fzo1fzo0n0  10118  fzoaddel  10127  exbtwnz  10186  flid  10219  flqaddz  10232  flqdiv  10256  modqid  10284  frec2uzf1od  10341  iseqf1olemqk  10429  bcval5  10676  abs2difabs  11050  fzomaxdiflem  11054  icodiamlt  11122  dfabsmax  11159  rexico  11163  mul0inf  11182  xrbdtri  11217  sumeq2  11300  sumsnf  11350  fsum00  11403  prodeq2  11498  prodsnf  11533  zsupcllemstep  11878  zssinfcl  11881  gcd0id  11912  gcdneg  11915  nn0seqcvgd  11973  lcmval  11995  lcmneg  12006  qredeq  12028  prmind2  12052  pw2dvdseu  12100  hashdvds  12153  pcpremul  12225  pcidlem  12254  pcgcd1  12259  fldivp1  12278  pcfaclem  12279  ennnfonelemex  12347  ennnfonelemnn0  12355  tgcl  12704  distop  12725  epttop  12730  neiss  12790  opnneissb  12795  ssnei2  12797  innei  12803  lmconst  12856  cnpnei  12859  cnptopco  12862  cnss1  12866  cnss2  12867  cncnpi  12868  cncnp  12870  cnconst2  12873  cnrest  12875  cnptopresti  12878  cnpdis  12882  lmtopcnp  12890  neitx  12908  tx1cn  12909  tx2cn  12910  txcnp  12911  txcnmpt  12913  txdis1cn  12918  psmetsym  12969  psmetres2  12973  isxmetd  12987  xmetsym  13008  xmetpsmet  13009  metrtri  13017  xblss2ps  13044  xblss2  13045  xblcntrps  13053  xblcntr  13054  bdxmet  13141  bdmet  13142  bdmopn  13144  xmetxp  13147  xmetxpbl  13148  rescncf  13208  cncfco  13218  mulcncflem  13230  mulcncf  13231  suplociccreex  13242  ivthinclemlopn  13254  ivthinclemuopn  13256  cnplimcim  13276  cnplimclemr  13278  limccnpcntop  13284  limccnp2cntop  13286  limccoap  13287  dvidlemap  13300  dvcn  13304  dvaddxxbr  13305  dvmulxxbr  13306  dvcoapbr  13311  dvcjbr  13312  dvrecap  13317  rpabscxpbnd  13499  lgsdirprm  13575  2sqlem8  13599  refeq  13907  apdifflemf  13925