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  10323  ixxss2  10324  ixxss12  10325  ubioc1  10348  lbico1  10349  lbicc2  10403  ubicc2  10404  lincmble  10423  elicod  10716  modqelico  10792  zmodfz  10804  modqmuladdim  10825  addmodid  10830  phicl2  13021  4sqlem12  13210  isstruct2r  13421  issubmd  13840  mndissubm  13841  submid  13843  subsubm  13849  0subm  13850  mhmima  13857  mhmeql  13858  issubgrpd2  14052  grpissubg  14056  subgintm  14060  nmzsubg  14072  eqger  14086  eqgcpbl  14090  ghmrn  14119  ghmpreima  14128  cntzsubm  14170  unitsubm  14535  subrgsubm  14651  subrgugrp  14657  subrgintm  14660  islssmd  14805  lsssubg  14823  islss4  14828  issubrgd  14898  lidlsubg  14932  2idlcpblrng  14969  mplsubgfi  15248  mplsubrgfi  15250  lmtopcnp  15509  xmeter  15695  tgqioo  15814  suplociccreex  15883  dedekindicc  15892  ivthinclemlopn  15895  ivthinclemuopn  15897  sin0pilem2  16042  pilem3  16043  coseq0q4123  16094  log2tlbndlog2  16253  uhgrissubgr  16740  egrsubgr  16742  uhgrspansubgr  16756  wlkres  16858