Theorem ifboth 3977

Description: A wff containing a conditional operator is true when both of its cases are true. (Contributed by NM, 3-Sep-2006.) (Revised by Mario Carneiro, 15-Feb-2015.)

Hypotheses

Ref	Expression
ifboth.1
ifboth.2

Assertion

Ref	Expression
ifboth

Proof of Theorem ifboth

Step	Hyp	Ref	Expression
1		ifboth.1	. 2
2		ifboth.2	. 2
3		simpll 753	. 2
4		simplr 755	. 2
5	1, 2, 3, 4	ifbothda 3976	1

Syntax hints:  -.wn 3  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  ifcif 3941

This theorem is referenced by:  ifcl  3983  keephyp  4006  soltmin  5411  xrmaxlt  11411  xrltmin  11412  xrmaxle  11413  xrlemin  11414  ifle  11425  expmulnbnd  12298  limsupgre  13304  isumless  13657  cvgrat  13692  rpnnen2lem4  13951  ruclem2  13965  sadcaddlem  14107  sadadd3  14111  pcmptdvds  14413  prmreclem5  14438  prmreclem6  14439  pnfnei  19721  mnfnei  19722  xkopt  20156  xmetrtri2  20859  stdbdxmet  21018  stdbdmet  21019  stdbdmopn  21021  xrsxmet  21314  icccmplem2  21328  metdscn  21360  metnrmlem1a  21362  ivthlem2  21864  ovolicc2lem5  21932  ioombl1lem1  21968  ioombl1lem4  21971  ismbfd  22047  mbfi1fseqlem4  22125  mbfi1fseqlem5  22126  itg2const  22147  itg2const2  22148  itg2monolem3  22159  itg2gt0  22167  itg2cnlem1  22168  itg2cnlem2  22169  iblss  22211  itgless  22223  ibladdlem  22226  iblabsr  22236  iblmulc2  22237  dvferm1lem  22385  dvferm2lem  22387  dvlip2  22396  dgradd2  22665  plydiveu  22694  chtppilim  23660  dchrvmasumiflem1  23686  ostth3  23823  mblfinlem2  30052  itg2addnclem  30066  itg2addnc  30069  itg2gt0cn  30070  ibladdnclem  30071  iblmulc2nc  30080  bddiblnc  30085  ftc1anclem5  30094  ftc1anclem8  30097  ftc1anc  30098

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