Theorem ifboth 4521

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

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

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 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-if 4482

This theorem is used by:  ifcl  4527  keephyp  4553  soltmin  6124  xrmaxlt  13281  xrltmin  13282  xrmaxle  13283  xrlemin  13284  ifle  13297  expmulnbnd  14347  limsupgre  15616  isumless  15982  cvgrat  16020  rpnnen2lem4  16353  ruclem2  16368  sadcaddlem  16595  sadadd3  16599  pcmptdvds  17034  prmreclem5  17060  prmreclem6  17061  pnfnei  23500  mnfnei  23501  xkopt  23936  xmetrtri2  24637  stdbdxmet  24796  stdbdmet  24797  stdbdmopn  24799  xrsxmet  25091  icccmplem2  25105  metdscn  25138  metnrmlem1a  25140  ivthlem2  25735  ovolicc2lem5  25804  ioombl1lem1  25841  ioombl1lem4  25844  ismbfd  25922  mbfi1fseqlem4  26001  mbfi1fseqlem5  26002  itg2const  26023  itg2const2  26024  itg2monolem3  26035  itg2gt0  26043  itg2cnlem1  26044  itg2cnlem2  26045  iblss  26087  itgless  26099  ibladdlem  26102  iblabsr  26112  iblmulc2  26113  bddiblnc  26124  dvferm1lem  26266  dvferm2lem  26268  dvlip2  26277  dgradd2  26549  plydiveu  26583  chtppilim  27766  dchrvmasumiflem1  27792  ostth3  27929  1smat1  34370  poimirlem24  38482  mblfinlem2  38496  itg2addnclem  38509  itg2addnc  38512  itg2gt0cn  38513  ibladdnclem  38514  iblmulc2nc  38523  ftc1anclem5  38535  ftc1anclem8  38538  ftc1anc  38539