Theorem ifbothda 4123

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

Hypotheses

Ref	Expression
ifboth.1	|- ( A = if ( ph , A , B ) -> ( ps <-> th ) )
ifboth.2	|- ( B = if ( ph , A , B ) -> ( ch <-> th ) )
ifbothda.3	|- ( ( et /\ ph ) -> ps )
ifbothda.4	|- ( ( et /\ -. ph ) -> ch )

Assertion

Ref	Expression
ifbothda	|- ( et -> th )

Proof of Theorem ifbothda

Step	Hyp	Ref	Expression
1		ifbothda.3	. . 3 |- ( ( et /\ ph ) -> ps )
2		iftrue 4092	. . . . . 6 |- ( ph -> if ( ph , A , B ) = A )
3	2	eqcomd 2628	. . . . 5 |- ( ph -> A = if ( ph , A , B ) )
4		ifboth.1	. . . . 5 |- ( A = if ( ph , A , B ) -> ( ps <-> th ) )
5	3, 4	syl 17	. . . 4 |- ( ph -> ( ps <-> th ) )
6	5	adantl 482	. . 3 |- ( ( et /\ ph ) -> ( ps <-> th ) )
7	1, 6	mpbid 222	. 2 |- ( ( et /\ ph ) -> th )
8		ifbothda.4	. . 3 |- ( ( et /\ -. ph ) -> ch )
9		iffalse 4095	. . . . . 6 |- ( -. ph -> if ( ph , A , B ) = B )
10	9	eqcomd 2628	. . . . 5 |- ( -. ph -> B = if ( ph , A , B ) )
11		ifboth.2	. . . . 5 |- ( B = if ( ph , A , B ) -> ( ch <-> th ) )
12	10, 11	syl 17	. . . 4 |- ( -. ph -> ( ch <-> th ) )
13	12	adantl 482	. . 3 |- ( ( et /\ -. ph ) -> ( ch <-> th ) )
14	8, 13	mpbid 222	. 2 |- ( ( et /\ -. ph ) -> th )
15	7, 14	pm2.61dan 832	1 |- ( et -> th )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   ifcif 4086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-if 4087

This theorem is referenced by:  ifboth  4124  resixpfo  7946  boxriin  7950  boxcutc  7951  suppr  8377  infpr  8409  cantnflem1  8586  ttukeylem5  9335  ttukeylem6  9336  bitsinv1lem  15163  bitsinv1  15164  smumullem  15214  hashgcdeq  15494  ramcl2lem  15713  acsfn  16320  tsrlemax  17220  odlem1  17954  gexlem1  17994  cyggex2  18298  dprdfeq0  18421  mplmon2  19493  evlslem1  19515  coe1tmmul2  19646  coe1tmmul  19647  xrsdsreclb  19793  ptcld  21416  xkopt  21458  stdbdxmet  22320  xrsxmet  22612  iccpnfcnv  22743  iccpnfhmeo  22744  xrhmeo  22745  dvcobr  23709  mdegle0  23837  dvradcnv  24175  psercnlem1  24179  psercn  24180  logtayl  24406  efrlim  24696  lgamgulmlem5  24759  musum  24917  dchrmulid2  24977  dchrsum2  24993  sumdchr2  24995  dchrisum0flblem1  25197  dchrisum0flblem2  25198  rplogsum  25216  pntlemj  25292  eupth2lem1  27078  eulerpathpr  27100  ifeqeqx  29361  xrge0iifcnv  29979  xrge0iifhom  29983  esumpinfval  30135  dstfrvunirn  30536  sgn3da  30603  plymulx0  30624  signswn0  30637  signswch  30638  fnejoin2  32364  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem24  33433  cnambfre  33458  itg2addnclem  33461  itg2addnclem3  33463  itg2addnc  33464  itg2gt0cn  33465  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  kelac1  37633