Theorem ifboth 4520

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4481

This theorem is referenced by:  ifcl  4526  keephyp  4552  soltmin  6094  xrmaxlt  13101  xrltmin  13102  xrmaxle  13103  xrlemin  13104  ifle  13117  expmulnbnd  14163  limsupgre  15409  isumless  15773  cvgrat  15811  rpnnen2lem4  16147  ruclem2  16162  sadcaddlem  16389  sadadd3  16393  pcmptdvds  16827  prmreclem5  16853  prmreclem6  16854  pnfnei  23169  mnfnei  23170  xkopt  23604  xmetrtri2  24305  stdbdxmet  24464  stdbdmet  24465  stdbdmopn  24467  xrsxmet  24759  icccmplem2  24773  metdscn  24806  metnrmlem1a  24808  ivthlem2  25414  ovolicc2lem5  25483  ioombl1lem1  25520  ioombl1lem4  25523  ismbfd  25601  mbfi1fseqlem4  25680  mbfi1fseqlem5  25681  itg2const  25702  itg2const2  25703  itg2monolem3  25714  itg2gt0  25722  itg2cnlem1  25723  itg2cnlem2  25724  iblss  25767  itgless  25779  ibladdlem  25782  iblabsr  25792  iblmulc2  25793  bddiblnc  25804  dvferm1lem  25949  dvferm2lem  25951  dvlip2  25961  dgradd2  26235  plydiveu  26267  chtppilim  27447  dchrvmasumiflem1  27473  ostth3  27610  1smat1  33974  poimirlem24  37858  mblfinlem2  37872  itg2addnclem  37885  itg2addnc  37888  itg2gt0cn  37889  ibladdnclem  37890  iblmulc2nc  37899  ftc1anclem5  37911  ftc1anclem8  37914  ftc1anc  37915