Theorem ifboth 4495

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539  ifcif 4456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-if 4457

This theorem is referenced by:  ifcl  4501  keephyp  4527  soltmin  6030  xrmaxlt  12844  xrltmin  12845  xrmaxle  12846  xrlemin  12847  ifle  12860  expmulnbnd  13878  limsupgre  15118  isumless  15485  cvgrat  15523  rpnnen2lem4  15854  ruclem2  15869  sadcaddlem  16092  sadadd3  16096  pcmptdvds  16523  prmreclem5  16549  prmreclem6  16550  pnfnei  22279  mnfnei  22280  xkopt  22714  xmetrtri2  23417  stdbdxmet  23577  stdbdmet  23578  stdbdmopn  23580  xrsxmet  23878  icccmplem2  23892  metdscn  23925  metnrmlem1a  23927  ivthlem2  24521  ovolicc2lem5  24590  ioombl1lem1  24627  ioombl1lem4  24630  ismbfd  24708  mbfi1fseqlem4  24788  mbfi1fseqlem5  24789  itg2const  24810  itg2const2  24811  itg2monolem3  24822  itg2gt0  24830  itg2cnlem1  24831  itg2cnlem2  24832  iblss  24874  itgless  24886  ibladdlem  24889  iblabsr  24899  iblmulc2  24900  bddiblnc  24911  dvferm1lem  25053  dvferm2lem  25055  dvlip2  25064  dgradd2  25334  plydiveu  25363  chtppilim  26528  dchrvmasumiflem1  26554  ostth3  26691  1smat1  31656  poimirlem24  35728  mblfinlem2  35742  itg2addnclem  35755  itg2addnc  35758  itg2gt0cn  35759  ibladdnclem  35760  iblmulc2nc  35769  ftc1anclem5  35781  ftc1anclem8  35784  ftc1anc  35785