Theorem ifboth 4524

Description: A wff 𝜃 containing a conditional operator is true when both of its cases are true. (Contributed by NM, 3-Sep-2006.) (Revised by Mario Carneiro, 15-Feb-2015.)

Hypotheses

Ref	Expression
ifboth.1	⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜃))
ifboth.2	⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜃))

Assertion

Ref	Expression
ifboth	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem ifboth

Step	Hyp	Ref	Expression
1		ifboth.1	. 2 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜃))
2		ifboth.2	. 2 ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜃))
3		simpll 765	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜑) → 𝜓)
4		simplr 767	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ ¬ 𝜑) → 𝜒)
5	1, 2, 3, 4	ifbothda 4523	1 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541  ifcif 4485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-if 4486

This theorem is referenced by:  ifcl  4530  keephyp  4556  soltmin  6089  xrmaxlt  13097  xrltmin  13098  xrmaxle  13099  xrlemin  13100  ifle  13113  expmulnbnd  14135  limsupgre  15360  isumless  15727  cvgrat  15765  rpnnen2lem4  16096  ruclem2  16111  sadcaddlem  16334  sadadd3  16338  pcmptdvds  16763  prmreclem5  16789  prmreclem6  16790  pnfnei  22567  mnfnei  22568  xkopt  23002  xmetrtri2  23705  stdbdxmet  23867  stdbdmet  23868  stdbdmopn  23870  xrsxmet  24168  icccmplem2  24182  metdscn  24215  metnrmlem1a  24217  ivthlem2  24812  ovolicc2lem5  24881  ioombl1lem1  24918  ioombl1lem4  24921  ismbfd  24999  mbfi1fseqlem4  25079  mbfi1fseqlem5  25080  itg2const  25101  itg2const2  25102  itg2monolem3  25113  itg2gt0  25121  itg2cnlem1  25122  itg2cnlem2  25123  iblss  25165  itgless  25177  ibladdlem  25180  iblabsr  25190  iblmulc2  25191  bddiblnc  25202  dvferm1lem  25344  dvferm2lem  25346  dvlip2  25355  dgradd2  25625  plydiveu  25654  chtppilim  26819  dchrvmasumiflem1  26845  ostth3  26982  1smat1  32276  poimirlem24  36091  mblfinlem2  36105  itg2addnclem  36118  itg2addnc  36121  itg2gt0cn  36122  ibladdnclem  36123  iblmulc2nc  36132  ftc1anclem5  36144  ftc1anclem8  36147  ftc1anc  36148