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  10182  ixxss2  10183  ixxss12  10184  ubioc1  10207  lbico1  10208  lbicc2  10262  ubicc2  10263  elicod  10568  modqelico  10640  zmodfz  10652  modqmuladdim  10673  addmodid  10678  phicl2  12847  4sqlem12  13036  isstruct2r  13154  issubmd  13618  mndissubm  13619  submid  13621  subsubm  13627  0subm  13628  mhmima  13635  mhmeql  13636  issubgrpd2  13838  grpissubg  13842  subgintm  13846  nmzsubg  13858  eqger  13872  eqgcpbl  13876  ghmrn  13905  ghmpreima  13914  unitsubm  14195  subrgsubm  14310  subrgugrp  14316  subrgintm  14319  islssmd  14435  lsssubg  14453  islss4  14458  issubrgd  14528  lidlsubg  14562  2idlcpblrng  14599  mplsubgfi  14782  lmtopcnp  15041  xmeter  15227  tgqioo  15346  suplociccreex  15415  dedekindicc  15424  ivthinclemlopn  15427  ivthinclemuopn  15429  sin0pilem2  15573  pilem3  15574  coseq0q4123  15625  uhgrissubgr  16182  egrsubgr  16184  uhgrspansubgr  16198  wlkres  16300