Theorem ifboth 4514

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-if 4475

This theorem is referenced by:  ifcl  4520  keephyp  4546  soltmin  6113  xrmaxlt  13174  xrltmin  13175  xrmaxle  13176  xrlemin  13177  ifle  13190  expmulnbnd  14238  limsupgre  15484  isumless  15851  cvgrat  15889  rpnnen2lem4  16225  ruclem2  16240  sadcaddlem  16467  sadadd3  16471  pcmptdvds  16906  prmreclem5  16932  prmreclem6  16933  pnfnei  23253  mnfnei  23254  xkopt  23688  xmetrtri2  24389  stdbdxmet  24548  stdbdmet  24549  stdbdmopn  24551  xrsxmet  24843  icccmplem2  24857  metdscn  24890  metnrmlem1a  24892  ivthlem2  25487  ovolicc2lem5  25556  ioombl1lem1  25593  ioombl1lem4  25596  ismbfd  25674  mbfi1fseqlem4  25753  mbfi1fseqlem5  25754  itg2const  25775  itg2const2  25776  itg2monolem3  25787  itg2gt0  25795  itg2cnlem1  25796  itg2cnlem2  25797  iblss  25840  itgless  25852  ibladdlem  25855  iblabsr  25865  iblmulc2  25866  bddiblnc  25877  dvferm1lem  26019  dvferm2lem  26021  dvlip2  26030  dgradd2  26301  plydiveu  26332  chtppilim  27509  dchrvmasumiflem1  27535  ostth3  27672  1smat1  34055  poimirlem24  38091  mblfinlem2  38105  itg2addnclem  38118  itg2addnc  38121  itg2gt0cn  38122  ibladdnclem  38123  iblmulc2nc  38132  ftc1anclem5  38144  ftc1anclem8  38147  ftc1anc  38148