Theorem ifboth 4540

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ifcif 4500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-if 4501

This theorem is referenced by:  ifcl  4546  keephyp  4572  soltmin  6125  xrmaxlt  13195  xrltmin  13196  xrmaxle  13197  xrlemin  13198  ifle  13211  expmulnbnd  14251  limsupgre  15495  isumless  15859  cvgrat  15897  rpnnen2lem4  16233  ruclem2  16248  sadcaddlem  16474  sadadd3  16478  pcmptdvds  16912  prmreclem5  16938  prmreclem6  16939  pnfnei  23156  mnfnei  23157  xkopt  23591  xmetrtri2  24293  stdbdxmet  24452  stdbdmet  24453  stdbdmopn  24455  xrsxmet  24747  icccmplem2  24761  metdscn  24794  metnrmlem1a  24796  ivthlem2  25403  ovolicc2lem5  25472  ioombl1lem1  25509  ioombl1lem4  25512  ismbfd  25590  mbfi1fseqlem4  25669  mbfi1fseqlem5  25670  itg2const  25691  itg2const2  25692  itg2monolem3  25703  itg2gt0  25711  itg2cnlem1  25712  itg2cnlem2  25713  iblss  25756  itgless  25768  ibladdlem  25771  iblabsr  25781  iblmulc2  25782  bddiblnc  25793  dvferm1lem  25938  dvferm2lem  25940  dvlip2  25950  dgradd2  26224  plydiveu  26256  chtppilim  27436  dchrvmasumiflem1  27462  ostth3  27599  1smat1  33781  poimirlem24  37614  mblfinlem2  37628  itg2addnclem  37641  itg2addnc  37644  itg2gt0cn  37645  ibladdnclem  37646  iblmulc2nc  37655  ftc1anclem5  37667  ftc1anclem8  37670  ftc1anc  37671