Theorem ifboth 4532

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570  ifcif 4492

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-if 4493

This theorem is used by:  ifcl  4538  keephyp  4564  soltmin  6141  xrmaxlt  13225  xrltmin  13226  xrmaxle  13227  xrlemin  13228  ifle  13241  expmulnbnd  14291  limsupgre  15558  isumless  15925  cvgrat  15963  rpnnen2lem4  16298  ruclem2  16313  sadcaddlem  16540  sadadd3  16544  pcmptdvds  16979  prmreclem5  17005  prmreclem6  17006  pnfnei  23414  mnfnei  23415  xkopt  23849  xmetrtri2  24550  stdbdxmet  24709  stdbdmet  24710  stdbdmopn  24712  xrsxmet  25004  icccmplem2  25018  metdscn  25051  metnrmlem1a  25053  ivthlem2  25648  ovolicc2lem5  25717  ioombl1lem1  25754  ioombl1lem4  25757  ismbfd  25835  mbfi1fseqlem4  25914  mbfi1fseqlem5  25915  itg2const  25936  itg2const2  25937  itg2monolem3  25948  itg2gt0  25956  itg2cnlem1  25957  itg2cnlem2  25958  iblss  26001  itgless  26013  ibladdlem  26016  iblabsr  26026  iblmulc2  26027  bddiblnc  26038  dvferm1lem  26180  dvferm2lem  26182  dvlip2  26191  dgradd2  26462  plydiveu  26496  chtppilim  27676  dchrvmasumiflem1  27702  ostth3  27839  1smat1  34225  poimirlem24  38335  mblfinlem2  38349  itg2addnclem  38362  itg2addnc  38365  itg2gt0cn  38366  ibladdnclem  38367  iblmulc2nc  38376  ftc1anclem5  38388  ftc1anclem8  38391  ftc1anc  38392