Theorem ifboth 4587

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-if 4549

This theorem is referenced by:  ifcl  4593  keephyp  4619  soltmin  6168  xrmaxlt  13243  xrltmin  13244  xrmaxle  13245  xrlemin  13246  ifle  13259  expmulnbnd  14284  limsupgre  15527  isumless  15893  cvgrat  15931  rpnnen2lem4  16265  ruclem2  16280  sadcaddlem  16503  sadadd3  16507  pcmptdvds  16941  prmreclem5  16967  prmreclem6  16968  pnfnei  23249  mnfnei  23250  xkopt  23684  xmetrtri2  24387  stdbdxmet  24549  stdbdmet  24550  stdbdmopn  24552  xrsxmet  24850  icccmplem2  24864  metdscn  24897  metnrmlem1a  24899  ivthlem2  25506  ovolicc2lem5  25575  ioombl1lem1  25612  ioombl1lem4  25615  ismbfd  25693  mbfi1fseqlem4  25773  mbfi1fseqlem5  25774  itg2const  25795  itg2const2  25796  itg2monolem3  25807  itg2gt0  25815  itg2cnlem1  25816  itg2cnlem2  25817  iblss  25860  itgless  25872  ibladdlem  25875  iblabsr  25885  iblmulc2  25886  bddiblnc  25897  dvferm1lem  26042  dvferm2lem  26044  dvlip2  26054  dgradd2  26328  plydiveu  26358  chtppilim  27537  dchrvmasumiflem1  27563  ostth3  27700  1smat1  33750  poimirlem24  37604  mblfinlem2  37618  itg2addnclem  37631  itg2addnc  37634  itg2gt0cn  37635  ibladdnclem  37636  iblmulc2nc  37645  ftc1anclem5  37657  ftc1anclem8  37660  ftc1anc  37661