Theorem ifboth 4124

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1483  ifcif 4086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-if 4087

This theorem is referenced by:  ifcl  4130  keephyp  4152  soltmin  5532  xrmaxlt  12012  xrltmin  12013  xrmaxle  12014  xrlemin  12015  ifle  12028  expmulnbnd  12996  limsupgre  14212  isumless  14577  cvgrat  14615  rpnnen2lem4  14946  ruclem2  14961  sadcaddlem  15179  sadadd3  15183  pcmptdvds  15598  prmreclem5  15624  prmreclem6  15625  pnfnei  21024  mnfnei  21025  xkopt  21458  xmetrtri2  22161  stdbdxmet  22320  stdbdmet  22321  stdbdmopn  22323  xrsxmet  22612  icccmplem2  22626  metdscn  22659  metnrmlem1a  22661  ivthlem2  23221  ovolicc2lem5  23289  ioombl1lem1  23326  ioombl1lem4  23329  ismbfd  23407  mbfi1fseqlem4  23485  mbfi1fseqlem5  23486  itg2const  23507  itg2const2  23508  itg2monolem3  23519  itg2gt0  23527  itg2cnlem1  23528  itg2cnlem2  23529  iblss  23571  itgless  23583  ibladdlem  23586  iblabsr  23596  iblmulc2  23597  dvferm1lem  23747  dvferm2lem  23749  dvlip2  23758  dgradd2  24024  plydiveu  24053  chtppilim  25164  dchrvmasumiflem1  25190  ostth3  25327  1smat1  29870  poimirlem24  33433  mblfinlem2  33447  itg2addnclem  33461  itg2addnc  33464  itg2gt0cn  33465  ibladdnclem  33466  iblmulc2nc  33475  bddiblnc  33480  ftc1anclem5  33489  ftc1anclem8  33492  ftc1anc  33493