MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ifeqda Structured version   Unicode version

Theorem ifeqda 3962
Description: Separation of the values of the conditional operator. (Contributed by Alexander van der Vekens, 13-Apr-2018.)
Hypotheses
Ref Expression
ifeqda.1  |-  ( (
ph  /\  ps )  ->  A  =  C )
ifeqda.2  |-  ( (
ph  /\  -.  ps )  ->  B  =  C )
Assertion
Ref Expression
ifeqda  |-  ( ph  ->  if ( ps ,  A ,  B )  =  C )

Proof of Theorem ifeqda
StepHypRef Expression
1 iftrue 3935 . . . 4  |-  ( ps 
->  if ( ps ,  A ,  B )  =  A )
21adantl 464 . . 3  |-  ( (
ph  /\  ps )  ->  if ( ps ,  A ,  B )  =  A )
3 ifeqda.1 . . 3  |-  ( (
ph  /\  ps )  ->  A  =  C )
42, 3eqtrd 2495 . 2  |-  ( (
ph  /\  ps )  ->  if ( ps ,  A ,  B )  =  C )
5 iffalse 3938 . . . 4  |-  ( -. 
ps  ->  if ( ps ,  A ,  B
)  =  B )
65adantl 464 . . 3  |-  ( (
ph  /\  -.  ps )  ->  if ( ps ,  A ,  B )  =  B )
7 ifeqda.2 . . 3  |-  ( (
ph  /\  -.  ps )  ->  B  =  C )
86, 7eqtrd 2495 . 2  |-  ( (
ph  /\  -.  ps )  ->  if ( ps ,  A ,  B )  =  C )
94, 8pm2.61dan 789 1  |-  ( ph  ->  if ( ps ,  A ,  B )  =  C )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 367    = wceq 1398   ifcif 3929
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-if 3930
This theorem is referenced by:  somincom  5389  cantnfp1  8091  ccatsymb  12589  swrdccat3blem  12711  repswccat  12748  ccatco  12792  bitsinvp1  14183  xrsdsreval  18658  fvmptnn04if  19517  chfacfscmulgsum  19528  chfacfpmmulgsum  19532  oprpiece1res2  21618  phtpycc  21657  atantayl2  23466  ccatmulgnn0dir  28760  plymulx  28769  elmrsubrn  29144  fourierdlem101  32229  linc0scn0  33278  m1modmmod  33388  digexp  33482
  Copyright terms: Public domain W3C validator