Theorem mpbir3and 1207

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 1204	. 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 1005

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 1007

This theorem is referenced by:  ixxss1  10260  ixxss2  10261  ixxss12  10262  ubioc1  10285  lbico1  10286  lbicc2  10340  ubicc2  10341  lincmble  10360  elicod  10652  modqelico  10724  zmodfz  10736  modqmuladdim  10757  addmodid  10762  phicl2  12941  4sqlem12  13130  isstruct2r  13312  issubmd  13734  mndissubm  13735  submid  13737  subsubm  13743  0subm  13744  mhmima  13751  mhmeql  13752  issubgrpd2  13948  grpissubg  13952  subgintm  13956  nmzsubg  13968  eqger  13982  eqgcpbl  13986  ghmrn  14015  ghmpreima  14024  unitsubm  14369  subrgsubm  14485  subrgugrp  14491  subrgintm  14494  islssmd  14638  lsssubg  14656  islss4  14661  issubrgd  14731  lidlsubg  14765  2idlcpblrng  14802  mplsubgfi  14987  lmtopcnp  15246  xmeter  15432  tgqioo  15551  suplociccreex  15620  dedekindicc  15629  ivthinclemlopn  15632  ivthinclemuopn  15634  sin0pilem2  15778  pilem3  15779  coseq0q4123  15830  uhgrissubgr  16387  egrsubgr  16389  uhgrspansubgr  16403  wlkres  16505