Theorem iftruei 3898

Description: Inference associated with iftrue 3897. (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 3897	. 2 |- ( ph -> if ( ph , A , B ) = A )
3	1, 2	ax-mp 5	1 |- if ( ph , A , B ) = A

Syntax hints:   = wceq 1370   ifcif 3891

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-if 3892

This theorem is referenced by:  oe0m  7060  ttukeylem4  8784  xnegpnf  11282  xnegmnf  11283  xaddpnf1  11299  xaddpnf2  11300  xaddmnf1  11301  xaddmnf2  11302  pnfaddmnf  11303  mnfaddpnf  11304  xmul01  11333  exp0  11972  swrd00  12418  sgn0  12682  mulg0  15736  mvrid  17605  zzngim  18096  obsipid  18258  mamulid  18415  mamurid  18416  mdetdiagid  18524  fclscmpi  19720  ioorinv  21174  ig1pval2  21763  dgrcolem2  21859  plydivlem4  21880  vieta1lem2  21895  0cxp  22229  cxpexp  22231  lgs0  22766  lgs2  22770  axlowdim  23344  gx0  23885  rdgprc0  27743  refsum2cnlem1  29899  mat1dimid  31026  cpdmatlem3  31296  cpidmat  31303  bj-pr11val  32800  bj-pr22val  32814  mapdhval0  35678  hdmap1val0  35753