Theorem iftruei 3948

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

Hypothesis

Ref	Expression
iftruei.1

Assertion

Ref	Expression
iftruei

Proof of Theorem iftruei

Step	Hyp	Ref	Expression
1		iftruei.1	. 2
2		iftrue 3947	. 2
3	1, 2	ax-mp 5	1

Syntax hints:  =wceq 1395  ifcif 3941

This theorem is referenced by:  oe0m  7187  ttukeylem4  8913  xnegpnf  11437  xnegmnf  11438  xaddpnf1  11454  xaddpnf2  11455  xaddmnf1  11456  xaddmnf2  11457  pnfaddmnf  11458  mnfaddpnf  11459  xmul01  11488  exp0  12170  swrd00  12645  sgn0  12922  mulg0  16147  mvrid  18079  zzngim  18591  obsipid  18753  mamulid  18943  mamurid  18944  mat1dimid  18976  scmatf1  19033  mdetdiagid  19102  chpdmatlem3  19341  chpidmat  19348  fclscmpi  20530  ioorinv  21985  ig1pval2  22574  dgrcolem2  22671  plydivlem4  22692  vieta1lem2  22707  0cxp  23047  cxpexp  23049  lgs0  23584  lgs2  23588  axlowdim  24264  gx0  25263  signsw0glem  28510  rdgprc0  29226  lcm0val  31200  refsum2cnlem1  31412  cncfiooicclem1  31696  fouriersw  32014  bj-pr11val  34563  bj-pr22val  34577  mapdhval0  37452  hdmap1val0  37527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-if 3942