Theorem iftruei 3864

Description: Inference associated with iftrue 3863. (Contributed by BJ, 7-Oct-2018.)

Hypothesis

Ref	Expression
iftruei.1	|- ph

Assertion

Ref	Expression
iftruei	|- if ( ph , A , B ) = A

Proof of Theorem iftruei

Step	Hyp	Ref	Expression
1		iftruei.1	. 2 |- ph
2		iftrue 3863	. 2 |- ( ph -> if ( ph , A , B ) = A )
3	1, 2	ax-mp 5	1 |- if ( ph , A , B ) = A

Syntax hints:   = wceq 1399   ifcif 3857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-if 3858

This theorem is referenced by:  oe0m  7086  ttukeylem4  8805  xnegpnf  11329  xnegmnf  11330  xaddpnf1  11346  xaddpnf2  11347  xaddmnf1  11348  xaddmnf2  11349  pnfaddmnf  11350  mnfaddpnf  11351  xmul01  11380  exp0  12073  swrd00  12554  sgn0  12924  mulg0  16264  mvrid  18192  zzngim  18682  obsipid  18844  mamulid  19028  mamurid  19029  mat1dimid  19061  scmatf1  19118  mdetdiagid  19187  chpdmatlem3  19426  chpidmat  19433  fclscmpi  20615  ioorinv  22070  ig1pval2  22659  dgrcolem2  22756  plydivlem4  22777  vieta1lem2  22792  0cxp  23134  cxpexp  23136  lgs0  23701  lgs2  23705  axlowdim  24385  gx0  25380  signsw0glem  28693  rdgprc0  29391  lcm0val  31368  refsum2cnlem1  31579  cncfiooicclem1  31862  fouriersw  32180  blen0  33393  0dig1  33430  bj-pr11val  34911  bj-pr22val  34925  mapdhval0  37865  hdmap1val0  37940