Theorem ifboth 4074

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475  ifcif 4036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-if 4037

This theorem is referenced by:  ifcl  4080  keephyp  4102  soltmin  5451  xrmaxlt  11886  xrltmin  11887  xrmaxle  11888  xrlemin  11889  ifle  11902  expmulnbnd  12858  limsupgre  14060  isumless  14416  cvgrat  14454  rpnnen2lem4  14785  ruclem2  14800  sadcaddlem  15017  sadadd3  15021  pcmptdvds  15436  prmreclem5  15462  prmreclem6  15463  pnfnei  20834  mnfnei  20835  xkopt  21268  xmetrtri2  21971  stdbdxmet  22130  stdbdmet  22131  stdbdmopn  22133  xrsxmet  22420  icccmplem2  22434  metdscn  22467  metnrmlem1a  22469  ivthlem2  23028  ovolicc2lem5  23096  ioombl1lem1  23133  ioombl1lem4  23136  ismbfd  23213  mbfi1fseqlem4  23291  mbfi1fseqlem5  23292  itg2const  23313  itg2const2  23314  itg2monolem3  23325  itg2gt0  23333  itg2cnlem1  23334  itg2cnlem2  23335  iblss  23377  itgless  23389  ibladdlem  23392  iblabsr  23402  iblmulc2  23403  dvferm1lem  23551  dvferm2lem  23553  dvlip2  23562  dgradd2  23828  plydiveu  23857  chtppilim  24964  dchrvmasumiflem1  24990  ostth3  25127  1smat1  29198  poimirlem24  32603  mblfinlem2  32617  itg2addnclem  32631  itg2addnc  32634  itg2gt0cn  32635  ibladdnclem  32636  iblmulc2nc  32645  bddiblnc  32650  ftc1anclem5  32659  ftc1anclem8  32662  ftc1anc  32663