Theorem ifboth 4478

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 767	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜑) → 𝜓)
4		simplr 769	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ ¬ 𝜑) → 𝜒)
5	1, 2, 3, 4	ifbothda 4477	1 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1543  ifcif 4439

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-if 4440

This theorem is referenced by:  ifcl  4484  keephyp  4510  soltmin  6001  xrmaxlt  12771  xrltmin  12772  xrmaxle  12773  xrlemin  12774  ifle  12787  expmulnbnd  13802  limsupgre  15042  isumless  15409  cvgrat  15447  rpnnen2lem4  15778  ruclem2  15793  sadcaddlem  16016  sadadd3  16020  pcmptdvds  16447  prmreclem5  16473  prmreclem6  16474  pnfnei  22117  mnfnei  22118  xkopt  22552  xmetrtri2  23254  stdbdxmet  23413  stdbdmet  23414  stdbdmopn  23416  xrsxmet  23706  icccmplem2  23720  metdscn  23753  metnrmlem1a  23755  ivthlem2  24349  ovolicc2lem5  24418  ioombl1lem1  24455  ioombl1lem4  24458  ismbfd  24536  mbfi1fseqlem4  24616  mbfi1fseqlem5  24617  itg2const  24638  itg2const2  24639  itg2monolem3  24650  itg2gt0  24658  itg2cnlem1  24659  itg2cnlem2  24660  iblss  24702  itgless  24714  ibladdlem  24717  iblabsr  24727  iblmulc2  24728  bddiblnc  24739  dvferm1lem  24881  dvferm2lem  24883  dvlip2  24892  dgradd2  25162  plydiveu  25191  chtppilim  26356  dchrvmasumiflem1  26382  ostth3  26519  1smat1  31468  poimirlem24  35538  mblfinlem2  35552  itg2addnclem  35565  itg2addnc  35568  itg2gt0cn  35569  ibladdnclem  35570  iblmulc2nc  35579  ftc1anclem5  35591  ftc1anclem8  35594  ftc1anc  35595