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  10256  ixxss2  10257  ixxss12  10258  ubioc1  10281  lbico1  10282  lbicc2  10336  ubicc2  10337  lincmble  10356  elicod  10648  modqelico  10720  zmodfz  10732  modqmuladdim  10753  addmodid  10758  phicl2  12936  4sqlem12  13125  isstruct2r  13307  issubmd  13771  mndissubm  13772  submid  13774  subsubm  13780  0subm  13781  mhmima  13788  mhmeql  13789  issubgrpd2  13991  grpissubg  13995  subgintm  13999  nmzsubg  14011  eqger  14025  eqgcpbl  14029  ghmrn  14058  ghmpreima  14067  unitsubm  14349  subrgsubm  14465  subrgugrp  14471  subrgintm  14474  islssmd  14619  lsssubg  14637  islss4  14642  issubrgd  14712  lidlsubg  14746  2idlcpblrng  14783  mplsubgfi  14968  lmtopcnp  15227  xmeter  15413  tgqioo  15532  suplociccreex  15601  dedekindicc  15610  ivthinclemlopn  15613  ivthinclemuopn  15615  sin0pilem2  15759  pilem3  15760  coseq0q4123  15811  uhgrissubgr  16368  egrsubgr  16370  uhgrspansubgr  16384  wlkres  16486