Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ifboth Structured version   Visualization version   GIF version

Theorem ifboth 4466
 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
StepHypRef Expression
1 ifboth.1 . 2 (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓𝜃))
2 ifboth.2 . 2 (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒𝜃))
3 simpll 766 . 2 (((𝜓𝜒) ∧ 𝜑) → 𝜓)
4 simplr 768 . 2 (((𝜓𝜒) ∧ ¬ 𝜑) → 𝜒)
51, 2, 3, 4ifbothda 4465 1 ((𝜓𝜒) → 𝜃)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  ifcif 4428 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-if 4429 This theorem is referenced by:  ifcl  4472  keephyp  4497  soltmin  5967  xrmaxlt  12582  xrltmin  12583  xrmaxle  12584  xrlemin  12585  ifle  12598  expmulnbnd  13612  limsupgre  14850  isumless  15212  cvgrat  15251  rpnnen2lem4  15582  ruclem2  15597  sadcaddlem  15816  sadadd3  15820  pcmptdvds  16240  prmreclem5  16266  prmreclem6  16267  pnfnei  21866  mnfnei  21867  xkopt  22301  xmetrtri2  23004  stdbdxmet  23163  stdbdmet  23164  stdbdmopn  23166  xrsxmet  23455  icccmplem2  23469  metdscn  23502  metnrmlem1a  23504  ivthlem2  24097  ovolicc2lem5  24166  ioombl1lem1  24203  ioombl1lem4  24206  ismbfd  24284  mbfi1fseqlem4  24363  mbfi1fseqlem5  24364  itg2const  24385  itg2const2  24386  itg2monolem3  24397  itg2gt0  24405  itg2cnlem1  24406  itg2cnlem2  24407  iblss  24449  itgless  24461  ibladdlem  24464  iblabsr  24474  iblmulc2  24475  bddiblnc  24486  dvferm1lem  24628  dvferm2lem  24630  dvlip2  24639  dgradd2  24909  plydiveu  24938  chtppilim  26103  dchrvmasumiflem1  26129  ostth3  26266  1smat1  31223  poimirlem24  35232  mblfinlem2  35246  itg2addnclem  35259  itg2addnc  35262  itg2gt0cn  35263  ibladdnclem  35264  iblmulc2nc  35273  ftc1anclem5  35285  ftc1anclem8  35288  ftc1anc  35289
 Copyright terms: Public domain W3C validator