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

Theorem ifboth 4157
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 805 . 2 (((𝜓𝜒) ∧ 𝜑) → 𝜓)
4 simplr 807 . 2 (((𝜓𝜒) ∧ ¬ 𝜑) → 𝜒)
51, 2, 3, 4ifbothda 4156 1 ((𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383   = wceq 1523  ifcif 4119
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-if 4120
This theorem is referenced by:  ifcl  4163  keephyp  4185  soltmin  5567  xrmaxlt  12050  xrltmin  12051  xrmaxle  12052  xrlemin  12053  ifle  12066  expmulnbnd  13036  limsupgre  14256  isumless  14621  cvgrat  14659  rpnnen2lem4  14990  ruclem2  15005  sadcaddlem  15226  sadadd3  15230  pcmptdvds  15645  prmreclem5  15671  prmreclem6  15672  pnfnei  21072  mnfnei  21073  xkopt  21506  xmetrtri2  22208  stdbdxmet  22367  stdbdmet  22368  stdbdmopn  22370  xrsxmet  22659  icccmplem2  22673  metdscn  22706  metnrmlem1a  22708  ivthlem2  23267  ovolicc2lem5  23335  ioombl1lem1  23372  ioombl1lem4  23375  ismbfd  23452  mbfi1fseqlem4  23530  mbfi1fseqlem5  23531  itg2const  23552  itg2const2  23553  itg2monolem3  23564  itg2gt0  23572  itg2cnlem1  23573  itg2cnlem2  23574  iblss  23616  itgless  23628  ibladdlem  23631  iblabsr  23641  iblmulc2  23642  dvferm1lem  23792  dvferm2lem  23794  dvlip2  23803  dgradd2  24069  plydiveu  24098  chtppilim  25209  dchrvmasumiflem1  25235  ostth3  25372  1smat1  29998  poimirlem24  33563  mblfinlem2  33577  itg2addnclem  33591  itg2addnc  33594  itg2gt0cn  33595  ibladdnclem  33596  iblmulc2nc  33605  bddiblnc  33610  ftc1anclem5  33619  ftc1anclem8  33622  ftc1anc  33623
  Copyright terms: Public domain W3C validator