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  10236  ixxss2  10237  ixxss12  10238  ubioc1  10261  lbico1  10262  lbicc2  10316  ubicc2  10317  lincmble  10336  elicod  10623  modqelico  10695  zmodfz  10707  modqmuladdim  10728  addmodid  10733  phicl2  12907  4sqlem12  13096  isstruct2r  13215  issubmd  13679  mndissubm  13680  submid  13682  subsubm  13688  0subm  13689  mhmima  13696  mhmeql  13697  issubgrpd2  13899  grpissubg  13903  subgintm  13907  nmzsubg  13919  eqger  13933  eqgcpbl  13937  ghmrn  13966  ghmpreima  13975  unitsubm  14256  subrgsubm  14371  subrgugrp  14377  subrgintm  14380  islssmd  14499  lsssubg  14517  islss4  14522  issubrgd  14592  lidlsubg  14626  2idlcpblrng  14663  mplsubgfi  14848  lmtopcnp  15107  xmeter  15293  tgqioo  15412  suplociccreex  15481  dedekindicc  15490  ivthinclemlopn  15493  ivthinclemuopn  15495  sin0pilem2  15639  pilem3  15640  coseq0q4123  15691  uhgrissubgr  16248  egrsubgr  16250  uhgrspansubgr  16264  wlkres  16366