Theorem iftruei 3879

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

Syntax hints:   = wceq 1452   ifcif 3872

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-if 3873

This theorem is referenced by:  oe0m  7238  ttukeylem4  8960  xnegpnf  11525  xnegmnf  11526  xaddpnf1  11542  xaddpnf2  11543  xaddmnf1  11544  xaddmnf2  11545  pnfaddmnf  11546  mnfaddpnf  11547  xmul01  11578  exp0  12314  swrd00  12828  sgn0  13229  lcm0val  14637  prmo2  15077  prmo3  15078  prmo5  15178  mulg0  16841  mvrid  18724  zzngim  19200  obsipid  19362  mamulid  19543  mamurid  19544  mat1dimid  19576  scmatf1  19633  mdetdiagid  19702  chpdmatlem3  19941  chpidmat  19948  fclscmpi  21122  ioorinv  22607  ioorinvOLD  22612  ig1pval2  23204  ig1pval2OLD  23210  dgrcolem2  23307  plydivlem4  23328  vieta1lem2  23343  0cxp  23690  cxpexp  23692  lgs0  24316  lgs2  24320  axlowdim  25070  gx0  26070  madjusmdetlem1  28727  signsw0glem  29514  rdgprc0  30511  bj-pr11val  31669  bj-pr22val  31683  mapdhval0  35364  hdmap1val0  35439  refsum2cnlem1  37421  cncfiooicclem1  37868  fouriersw  38207  hspmbllem1  38566  vtxvalsnop  39294  iedgvalsnop  39295  1loopgrvd2  39725  eupth2  40151  blen0  40891  0dig1  40928