Theorem ifboth 4503

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 4502	1 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1531  ifcif 4465

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1775  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-if 4466

This theorem is referenced by:  ifcl  4509  keephyp  4534  soltmin  5989  xrmaxlt  12566  xrltmin  12567  xrmaxle  12568  xrlemin  12569  ifle  12582  expmulnbnd  13588  limsupgre  14830  isumless  15192  cvgrat  15231  rpnnen2lem4  15562  ruclem2  15577  sadcaddlem  15798  sadadd3  15802  pcmptdvds  16222  prmreclem5  16248  prmreclem6  16249  pnfnei  21820  mnfnei  21821  xkopt  22255  xmetrtri2  22958  stdbdxmet  23117  stdbdmet  23118  stdbdmopn  23120  xrsxmet  23409  icccmplem2  23423  metdscn  23456  metnrmlem1a  23458  ivthlem2  24045  ovolicc2lem5  24114  ioombl1lem1  24151  ioombl1lem4  24154  ismbfd  24232  mbfi1fseqlem4  24311  mbfi1fseqlem5  24312  itg2const  24333  itg2const2  24334  itg2monolem3  24345  itg2gt0  24353  itg2cnlem1  24354  itg2cnlem2  24355  iblss  24397  itgless  24409  ibladdlem  24412  iblabsr  24422  iblmulc2  24423  dvferm1lem  24573  dvferm2lem  24575  dvlip2  24584  dgradd2  24850  plydiveu  24879  chtppilim  26043  dchrvmasumiflem1  26069  ostth3  26206  1smat1  31062  poimirlem24  34908  mblfinlem2  34922  itg2addnclem  34935  itg2addnc  34938  itg2gt0cn  34939  ibladdnclem  34940  iblmulc2nc  34949  bddiblnc  34954  ftc1anclem5  34963  ftc1anclem8  34966  ftc1anc  34967