Theorem ifboth 4569

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-if 4531

This theorem is referenced by:  ifcl  4575  keephyp  4601  soltmin  6158  xrmaxlt  13219  xrltmin  13220  xrmaxle  13221  xrlemin  13222  ifle  13235  expmulnbnd  14270  limsupgre  15513  isumless  15877  cvgrat  15915  rpnnen2lem4  16249  ruclem2  16264  sadcaddlem  16490  sadadd3  16494  pcmptdvds  16927  prmreclem5  16953  prmreclem6  16954  pnfnei  23243  mnfnei  23244  xkopt  23678  xmetrtri2  24381  stdbdxmet  24543  stdbdmet  24544  stdbdmopn  24546  xrsxmet  24844  icccmplem2  24858  metdscn  24891  metnrmlem1a  24893  ivthlem2  25500  ovolicc2lem5  25569  ioombl1lem1  25606  ioombl1lem4  25609  ismbfd  25687  mbfi1fseqlem4  25767  mbfi1fseqlem5  25768  itg2const  25789  itg2const2  25790  itg2monolem3  25801  itg2gt0  25809  itg2cnlem1  25810  itg2cnlem2  25811  iblss  25854  itgless  25866  ibladdlem  25869  iblabsr  25879  iblmulc2  25880  bddiblnc  25891  dvferm1lem  26036  dvferm2lem  26038  dvlip2  26048  dgradd2  26322  plydiveu  26354  chtppilim  27533  dchrvmasumiflem1  27559  ostth3  27696  1smat1  33764  poimirlem24  37630  mblfinlem2  37644  itg2addnclem  37657  itg2addnc  37660  itg2gt0cn  37661  ibladdnclem  37662  iblmulc2nc  37671  ftc1anclem5  37683  ftc1anclem8  37686  ftc1anc  37687