Theorem ifbieq2d 4111

Description: Equivalence/equality deduction for conditional operators. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypotheses

Ref	Expression
ifbieq2d.1	|- ( ph -> ( ps <-> ch ) )
ifbieq2d.2	|- ( ph -> A = B )

Assertion

Ref	Expression
ifbieq2d	|- ( ph -> if ( ps , C , A ) = if ( ch , C , B ) )

Proof of Theorem ifbieq2d

Step	Hyp	Ref	Expression
1		ifbieq2d.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	ifbid 4108	. 2 |- ( ph -> if ( ps , C , A ) = if ( ch , C , A ) )
3		ifbieq2d.2	. . 3 |- ( ph -> A = B )
4	3	ifeq2d 4105	. 2 |- ( ph -> if ( ch , C , A ) = if ( ch , C , B ) )
5	2, 4	eqtrd 2656	1 |- ( ph -> if ( ps , C , A ) = if ( ch , C , B ) )

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   ifcif 4086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-un 3579  df-if 4087

This theorem is referenced by:  tz7.44-2  7503  tz7.44-3  7504  oev  7594  cantnfp1lem1  8575  cantnfp1lem3  8577  fin23lem12  9153  fin23lem33  9167  axcc2  9259  ttukeylem3  9333  ttukey2g  9338  canthp1lem2  9475  canthp1  9476  xnegeq  12038  xaddval  12054  xmulval  12056  expval  12862  cshfn  13536  ofccat  13708  relexpsucnnr  13765  sgnval  13828  sadcp1  15177  smupp1  15202  gcdval  15218  gcdass  15264  lcmval  15305  lcmass  15327  lcmfval  15334  lcmf0val  15335  lcmfpr  15340  iserodd  15540  pcval  15549  vdwlem6  15690  ramub1lem2  15731  ramcl  15733  mulgval  17543  symgextfv  17838  symgfixfo  17859  odval  17953  submod  17984  gexval  17993  znval  19883  fvmptnn04if  20654  cpmadumatpoly  20688  cayleyhamilton  20695  cayleyhamiltonALT  20696  ptcmplem2  21857  iccpnfhmeo  22744  pcopt  22822  ioombl1  23330  ioorval  23342  uniioombllem6  23356  itg1addlem3  23465  itg2uba  23510  limcfval  23636  limcmpt  23647  limcco  23657  dvcobr  23709  ig1pval  23932  abelthlem9  24194  logtayllem  24405  logtayl  24406  leibpilem2  24668  rlimcnp2  24693  efrlim  24696  igamval  24773  muval  24858  lgsval  25026  lgsfval  25027  lgsval2lem  25032  rpvmasum2  25201  padicval  25306  padicabv  25319  axlowdimlem15  25836  axlowdim  25841  eupth2lem3lem3  27090  eupth2  27099  eucrct2eupth  27105  sgnsv  29727  sgnsval  29728  psgnfzto1stlem  29850  madjusmdetlem2  29894  madjusmdet  29897  xrge0iifcv  29980  xrge0iifhom  29983  xrge0tmdOLD  29991  xrge0tmd  29992  signspval  30629  rdgprc0  31699  dfrdg2  31701  dfrdg4  32058  csbrdgg  33175  finxpeq1  33223  finxpreclem3  33230  poimirlem1  33410  poimirlem7  33416  poimirlem10  33419  poimirlem11  33420  itg2addnclem  33461  itg2addnclem3  33463  itg2addnc  33464  fdc  33541  heiborlem4  33613  heiborlem6  33615  heiborlem10  33619  mapdhval  37013  hdmap1fval  37086  hdmap1vallem  37087  hdmap1val  37088  hdmap1cbv  37092  irrapxlem4  37389  clsk1indlem0  38339  clsk1indlem2  38340  clsk1indlem3  38341  clsk1indlem4  38342  clsk1indlem1  38343  dirkerval2  40311  dirkeritg  40319  dirkercncf  40324  fourierdlem29  40353  fourierdlem37  40361  fourierdlem62  40385  fourierdlem79  40402  fourierdlem81  40404  fourierdlem82  40405  fourierdlem92  40415  fourierdlem96  40419  fourierdlem97  40420  fourierdlem98  40421  fourierdlem99  40422  fourierdlem105  40428  fourierdlem108  40431  fourierdlem110  40433  fourierdlem112  40435  fourierdlem113  40436  fouriersw  40448  etransclem24  40475  etransclem25  40476  etransclem31  40482  etransclem35  40486  etransclem37  40488  sge0val  40583  nnfoctbdjlem  40672  nnfoctbdj  40673  ovnval  40755  ovnval2  40759  ovnval2b  40766  hsphoif  40790  hoidmvval  40791  hsphoival  40793  hoidmv1lelem1  40805  hoidmv1lelem2  40806  hoidmv1lelem3  40807  hoidmv1le  40808  ovnhoi  40817  hoidifhspval  40822  hspmbllem2  40841  ovnsubadd2  40860  blenval  42365