Theorem ifbothda 4156

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	⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜃))
ifboth.2	⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜃))
ifbothda.3	⊢ ((𝜂 ∧ 𝜑) → 𝜓)
ifbothda.4	⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜒)

Assertion

Ref	Expression
ifbothda	⊢ (𝜂 → 𝜃)

Proof of Theorem ifbothda

Step	Hyp	Ref	Expression
1		ifbothda.3	. . 3 ⊢ ((𝜂 ∧ 𝜑) → 𝜓)
2		iftrue 4125	. . . . . 6 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
3	2	eqcomd 2657	. . . . 5 ⊢ (𝜑 → 𝐴 = if(𝜑, 𝐴, 𝐵))
4		ifboth.1	. . . . 5 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜃))
5	3, 4	syl 17	. . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
6	5	adantl 481	. . 3 ⊢ ((𝜂 ∧ 𝜑) → (𝜓 ↔ 𝜃))
7	1, 6	mpbid 222	. 2 ⊢ ((𝜂 ∧ 𝜑) → 𝜃)
8		ifbothda.4	. . 3 ⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜒)
9		iffalse 4128	. . . . . 6 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
10	9	eqcomd 2657	. . . . 5 ⊢ (¬ 𝜑 → 𝐵 = if(𝜑, 𝐴, 𝐵))
11		ifboth.2	. . . . 5 ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜃))
12	10, 11	syl 17	. . . 4 ⊢ (¬ 𝜑 → (𝜒 ↔ 𝜃))
13	12	adantl 481	. . 3 ⊢ ((𝜂 ∧ ¬ 𝜑) → (𝜒 ↔ 𝜃))
14	8, 13	mpbid 222	. 2 ⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜃)
15	7, 14	pm2.61dan 849	1 ⊢ (𝜂 → 𝜃)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1523  ifcif 4119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-if 4120

This theorem is referenced by:  ifboth  4157  resixpfo  7988  boxriin  7992  boxcutc  7993  suppr  8418  infpr  8450  cantnflem1  8624  ttukeylem5  9373  ttukeylem6  9374  bitsinv1lem  15210  bitsinv1  15211  smumullem  15261  hashgcdeq  15541  ramcl2lem  15760  acsfn  16367  tsrlemax  17267  odlem1  18000  gexlem1  18040  cyggex2  18344  dprdfeq0  18467  mplmon2  19541  evlslem1  19563  coe1tmmul2  19694  coe1tmmul  19695  xrsdsreclb  19841  ptcld  21464  xkopt  21506  stdbdxmet  22367  xrsxmet  22659  iccpnfcnv  22790  iccpnfhmeo  22791  xrhmeo  22792  dvcobr  23754  mdegle0  23882  dvradcnv  24220  psercnlem1  24224  psercn  24225  logtayl  24451  efrlim  24741  lgamgulmlem5  24804  musum  24962  dchrmulid2  25022  dchrsum2  25038  sumdchr2  25040  dchrisum0flblem1  25242  dchrisum0flblem2  25243  rplogsum  25261  pntlemj  25337  eupth2lem1  27196  eulerpathpr  27218  ifeqeqx  29487  xrge0iifcnv  30107  xrge0iifhom  30111  esumpinfval  30263  dstfrvunirn  30664  sgn3da  30731  plymulx0  30752  signswn0  30765  signswch  30766  fnejoin2  32489  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  poimirlem24  33563  cnambfre  33588  itg2addnclem  33591  itg2addnclem3  33593  itg2addnc  33594  itg2gt0cn  33595  ftc1anclem7  33621  ftc1anclem8  33622  ftc1anc  33623  kelac1  37950