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

Theorem ifboth 4101
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 789 . 2 (((𝜓𝜒) ∧ 𝜑) → 𝜓)
4 simplr 791 . 2 (((𝜓𝜒) ∧ ¬ 𝜑) → 𝜒)
51, 2, 3, 4ifbothda 4100 1 ((𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384   = wceq 1480  ifcif 4063
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-if 4064
This theorem is referenced by:  ifcl  4107  keephyp  4129  soltmin  5496  xrmaxlt  11963  xrltmin  11964  xrmaxle  11965  xrlemin  11966  ifle  11979  expmulnbnd  12944  limsupgre  14154  isumless  14513  cvgrat  14551  rpnnen2lem4  14882  ruclem2  14897  sadcaddlem  15114  sadadd3  15118  pcmptdvds  15533  prmreclem5  15559  prmreclem6  15560  pnfnei  20947  mnfnei  20948  xkopt  21381  xmetrtri2  22084  stdbdxmet  22243  stdbdmet  22244  stdbdmopn  22246  xrsxmet  22535  icccmplem2  22549  metdscn  22582  metnrmlem1a  22584  ivthlem2  23144  ovolicc2lem5  23212  ioombl1lem1  23249  ioombl1lem4  23252  ismbfd  23330  mbfi1fseqlem4  23408  mbfi1fseqlem5  23409  itg2const  23430  itg2const2  23431  itg2monolem3  23442  itg2gt0  23450  itg2cnlem1  23451  itg2cnlem2  23452  iblss  23494  itgless  23506  ibladdlem  23509  iblabsr  23519  iblmulc2  23520  dvferm1lem  23668  dvferm2lem  23670  dvlip2  23679  dgradd2  23945  plydiveu  23974  chtppilim  25081  dchrvmasumiflem1  25107  ostth3  25244  1smat1  29676  poimirlem24  33100  mblfinlem2  33114  itg2addnclem  33128  itg2addnc  33131  itg2gt0cn  33132  ibladdnclem  33133  iblmulc2nc  33142  bddiblnc  33147  ftc1anclem5  33156  ftc1anclem8  33159  ftc1anc  33160
  Copyright terms: Public domain W3C validator