Theorem ifclda 3973

Description: Conditional closure. (Contributed by Jeff Madsen, 2-Sep-2009.)

Hypotheses

Ref	Expression
ifclda.1
ifclda.2

Assertion

Ref	Expression
ifclda

Proof of Theorem ifclda

Step	Hyp	Ref	Expression
1		iftrue 3947	. . . 4
2	1	adantl 466	. . 3
3		ifclda.1	. . 3
4	2, 3	eqeltrd 2545	. 2
5		iffalse 3950	. . . 4
6	5	adantl 466	. . 3
7		ifclda.2	. . 3
8	6, 7	eqeltrd 2545	. 2
9	4, 8	pm2.61dan 791	1

Syntax hints:  -.wn 3  ->wi 4  /\wa 369  =wceq 1395  e.wcel 1818  ifcif 3941

This theorem is referenced by:  unxpdomlem3  7746  acndom  8453  iunfictbso  8516  dfac12lem2  8545  ttukeylem6  8915  canthp1lem2  9052  xaddf  11452  xmulf  11493  ccatcl  12593  swrdcl  12646  ccatco  12801  lo1bdd2  13347  o1lo1  13360  sadadd2lem2  14100  sadcaddlem  14107  sadadd2lem  14109  sadadd3  14111  iserodd  14359  prmreclem2  14435  prmreclem4  14437  prmreclem6  14439  prmrec  14440  vdwlem6  14504  symgextf  16442  pmtrf  16480  cyggex2  16899  dprdfid  17057  dprdfidOLD  17064  dmdprdsplitlem  17084  dmdprdsplitlemOLD  17085  cygznlem1  18605  cygznlem2a  18606  cygznlem3  18608  cygth  18610  fvmptnn04if  19350  chfacfisf  19355  chfacfisfcpmat  19356  ptpjpre2  20081  ptopn2  20085  ptpjopn  20113  iccpnfcnv  21444  xrhmeo  21446  cmetcaulem  21727  ovolunlem1a  21907  ovolunlem1  21908  ioorf  21982  mbfi1fseqlem3  22124  mbfi1flim  22130  itg2seq  22149  itg2splitlem  22155  itg2split  22156  iblss  22211  itgle  22216  itgeqa  22220  ibladdlem  22226  itgaddlem1  22229  iblabslem  22234  iblabs  22235  iblabsr  22236  iblmulc2  22237  itgmulc2lem1  22238  bddmulibl  22245  itggt0  22248  itgcn  22249  ellimc2  22281  limccnp  22295  limccnp2  22296  dvcobr  22349  lhop1  22415  elplyd  22599  coeeq2  22639  dvply1  22680  aalioulem3  22730  dvtaylp  22765  dvradcnv  22816  psercnlem1  22820  logcnlem2  23024  logcnlem3  23025  logcnlem4  23026  logtayllem  23040  logtayl  23041  cxpcl  23055  recxpcl  23056  leibpilem2  23272  leibpi  23273  rlimcnp2  23296  efrlim  23299  pclogsum  23490  dchrelbasd  23514  lgsfcl2  23577  lgscllem  23578  lgsval2lem  23581  lgsne0  23608  dchrvmasumiflem2  23687  dchrisum0flblem1  23693  pntrlog2bndlem4  23765  pntrlog2bndlem5  23766  pntlemj  23788  padicabv  23815  sgnsval  27718  xrge0iifcnv  27915  xrge0iifhom  27919  pnfneige0  27933  esumpinfval  28079  sigaclfu2  28121  ballotlemsv  28448  ballotlemsdom  28450  signswmnd  28514  signsvvf  28536  signsvfn  28539  igamf  28593  igamcl  28594  mrsubcv  28870  mrsubff  28872  mrsubrn  28873  mrsubccat  28878  itg2addnclem2  30067  itg2gt0cn  30070  ibladdnclem  30071  itgaddnclem1  30073  iblabsnclem  30078  iblabsnc  30079  iblmulc2nc  30080  itgmulc2nclem1  30081  bddiblnc  30085  itggt0cn  30087  ftc1anclem5  30094  ftc1anclem6  30095  ftc1anclem7  30096  ftc1anclem8  30097  ftc1anc  30098  areacirc  30112  sdrgacs  31150  climsuse  31614  lptioo1  31638  icccncfext  31690  cncfiooicclem1  31696  iblsplit  31765  dirkerval2  31876  dirkerre  31877  fourierdlem9  31898  fourierdlem17  31906  fourierdlem43  31932  etransclem3  32020  etransclem7  32024  etransclem10  32027  etransclem21  32038  lincext1  33055  cdleme27cl  36092

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