Theorem ifbothda 3976

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

Hypotheses

Ref	Expression
ifboth.1
ifboth.2
ifbothda.3
ifbothda.4

Assertion

Ref	Expression
ifbothda

Proof of Theorem ifbothda

Step	Hyp	Ref	Expression
1		ifbothda.3	. . 3
2		iftrue 3947	. . . . . 6
3	2	eqcomd 2465	. . . . 5
4		ifboth.1	. . . . 5
5	3, 4	syl 16	. . . 4
6	5	adantl 466	. . 3
7	1, 6	mpbid 210	. 2
8		ifbothda.4	. . 3
9		iffalse 3950	. . . . . 6
10	9	eqcomd 2465	. . . . 5
11		ifboth.2	. . . . 5
12	10, 11	syl 16	. . . 4
13	12	adantl 466	. . 3
14	8, 13	mpbid 210	. 2
15	7, 14	pm2.61dan 791	1

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

This theorem is referenced by:  ifboth  3977  resixpfo  7527  boxriin  7531  boxcutc  7532  suppr  7950  cantnflem1  8129  cantnfp1OLD  8147  cantnflem1OLD  8152  ttukeylem5  8914  ttukeylem6  8915  bitsinv1lem  14091  bitsinv1  14092  smumullem  14142  ramcl2lem  14527  acsfn  15056  tsrlemax  15850  odlem1  16559  gexlem1  16599  cyggex2  16899  dprdfeq0  17062  dprdfeq0OLD  17069  mplmon2  18158  evlslem1  18184  coe1tmmul2  18317  coe1tmmul  18318  xrsdsreclb  18465  ptcld  20114  xkopt  20156  stdbdxmet  21018  xrsxmet  21314  iccpnfcnv  21444  iccpnfhmeo  21445  xrhmeo  21446  dvcobr  22349  mdegle0  22477  dvradcnv  22816  psercnlem1  22820  psercn  22821  logtayl  23041  efrlim  23299  musum  23467  dchrmulid2  23527  dchrsum2  23543  sumdchr2  23545  dchrisum0flblem1  23693  dchrisum0flblem2  23694  rplogsum  23712  pntlemj  23788  eupath2lem1  24977  eupath  24981  ifeqeqx  27419  xrge0iifcnv  27915  xrge0iifhom  27919  esumpinfval  28079  dstfrvunirn  28413  sgn3da  28480  plymulx0  28504  signswn0  28517  signswch  28518  lgamgulmlem5  28575  cnambfre  30063  itg2addnclem  30066  itg2addnclem3  30068  itg2addnc  30069  itg2gt0cn  30070  ftc1anclem7  30096  ftc1anclem8  30097  ftc1anc  30098  fnejoin2  30187  kelac1  31009  hashgcdeq  31158

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