Theorem mpbir3and 1182

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 1179	. 2 |- ( ph -> ( ch /\ th /\ ta ) )
5		mpbir3and.4	. 2 |- ( ph -> ( ps <-> ( ch /\ th /\ ta ) ) )
6	4, 5	mpbird 167	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   <-> wb 105   /\ w3a 980

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  df-3an 982

This theorem is referenced by:  ixxss1  9973  ixxss2  9974  ixxss12  9975  ubioc1  9998  lbico1  9999  lbicc2  10053  ubicc2  10054  elicod  10336  modqelico  10408  zmodfz  10420  modqmuladdim  10441  addmodid  10446  phicl2  12355  4sqlem12  12543  isstruct2r  12632  issubmd  13049  mndissubm  13050  submid  13052  subsubm  13058  0subm  13059  mhmima  13066  mhmeql  13067  issubgrpd2  13263  grpissubg  13267  subgintm  13271  nmzsubg  13283  eqger  13297  eqgcpbl  13301  ghmrn  13330  ghmpreima  13339  unitsubm  13618  subrgsubm  13733  subrgugrp  13739  subrgintm  13742  islssmd  13858  lsssubg  13876  islss4  13881  issubrgd  13951  lidlsubg  13985  2idlcpblrng  14022  lmtopcnp  14429  xmeter  14615  tgqioo  14734  suplociccreex  14803  dedekindicc  14812  ivthinclemlopn  14815  ivthinclemuopn  14817  sin0pilem2  14958  pilem3  14959  coseq0q4123  15010