Theorem mpbir3and 1211

Description: Detach a conjunction of truths in a biconditional. (Contributed by Mario Carneiro, 11-May-2014.)

Hypotheses

Ref	Expression
mpbir3and.1	|- ( ph -> ch )
mpbir3and.2	|- ( ph -> th )
mpbir3and.3	|- ( ph -> ta )
mpbir3and.4	|- ( ph -> ( ps <-> ( ch /\ th /\ ta ) ) )

Assertion

Ref	Expression
mpbir3and	|- ( ph -> ps )

Proof of Theorem mpbir3and

Step	Hyp	Ref	Expression
1		mpbir3and.1	. . 3 |- ( ph -> ch )
2		mpbir3and.2	. . 3 |- ( ph -> th )
3		mpbir3and.3	. . 3 |- ( ph -> ta )
4	1, 2, 3	3jca 1208	. 2 |- ( ph -> ( ch /\ th /\ ta ) )
5		mpbir3and.4	. 2 |- ( ph -> ( ps <-> ( ch /\ th /\ ta ) ) )
6	4, 5	mpbird 167	1 |- ( ph -> ps )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  ixxss1  10317  ixxss2  10318  ixxss12  10319  ubioc1  10342  lbico1  10343  lbicc2  10397  ubicc2  10398  lincmble  10417  elicod  10710  modqelico  10785  zmodfz  10797  modqmuladdim  10818  addmodid  10823  phicl2  13014  4sqlem12  13203  isstruct2r  13414  issubmd  13832  mndissubm  13833  submid  13835  subsubm  13841  0subm  13842  mhmima  13849  mhmeql  13850  issubgrpd2  14044  grpissubg  14048  subgintm  14052  nmzsubg  14064  eqger  14078  eqgcpbl  14082  ghmrn  14111  ghmpreima  14120  unitsubm  14477  subrgsubm  14593  subrgugrp  14599  subrgintm  14602  islssmd  14747  lsssubg  14765  islss4  14770  issubrgd  14840  lidlsubg  14874  2idlcpblrng  14911  mplsubgfi  15144  lmtopcnp  15403  xmeter  15589  tgqioo  15708  suplociccreex  15777  dedekindicc  15786  ivthinclemlopn  15789  ivthinclemuopn  15791  sin0pilem2  15936  pilem3  15937  coseq0q4123  15988  log2tlbndlog2  16142  uhgrissubgr  16624  egrsubgr  16626  uhgrspansubgr  16640  wlkres  16742