Theorem mpbir3and 1211

Description: Detach a conjunction of truths in a biconditional. (Contributed by Mario Carneiro, 11-May-2014.)

Hypotheses

Ref	Expression
mpbir3and.1	⊢ (𝜑 → 𝜒)
mpbir3and.2	⊢ (𝜑 → 𝜃)
mpbir3and.3	⊢ (𝜑 → 𝜏)
mpbir3and.4	⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏)))

Assertion

Ref	Expression
mpbir3and	⊢ (𝜑 → 𝜓)

Proof of Theorem mpbir3and

Step	Hyp	Ref	Expression
1		mpbir3and.1	. . 3 ⊢ (𝜑 → 𝜒)
2		mpbir3and.2	. . 3 ⊢ (𝜑 → 𝜃)
3		mpbir3and.3	. . 3 ⊢ (𝜑 → 𝜏)
4	1, 2, 3	3jca 1208	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃 ∧ 𝜏))
5		mpbir3and.4	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏)))
6	4, 5	mpbird 167	1 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  ixxss1  10324  ixxss2  10325  ixxss12  10326  ubioc1  10349  lbico1  10350  lbicc2  10404  ubicc2  10405  lincmble  10424  elicod  10717  modqelico  10793  zmodfz  10805  modqmuladdim  10826  addmodid  10831  phicl2  13022  4sqlem12  13211  isstruct2r  13422  issubmd  13841  mndissubm  13842  submid  13844  subsubm  13850  0subm  13851  mhmima  13858  mhmeql  13859  issubgrpd2  14053  grpissubg  14057  subgintm  14061  nmzsubg  14073  eqger  14087  eqgcpbl  14091  ghmrn  14120  ghmpreima  14129  cntzsubm  14171  unitsubm  14536  subrgsubm  14652  subrgugrp  14658  subrgintm  14661  islssmd  14806  lsssubg  14824  islss4  14829  issubrgd  14899  lidlsubg  14933  2idlcpblrng  14970  mplsubgfi  15229  lmtopcnp  15488  xmeter  15674  tgqioo  15793  suplociccreex  15862  dedekindicc  15871  ivthinclemlopn  15874  ivthinclemuopn  15876  sin0pilem2  16021  pilem3  16022  coseq0q4123  16073  log2tlbndlog2  16232  uhgrissubgr  16719  egrsubgr  16721  uhgrspansubgr  16735  wlkres  16837