Theorem ifbothda 4569

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 4537	. . . . . 6 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
3	2	eqcomd 2741	. . . . 5 ⊢ (𝜑 → 𝐴 = if(𝜑, 𝐴, 𝐵))
4		ifboth.1	. . . . 5 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜃))
5	3, 4	syl 17	. . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
6	5	adantl 481	. . 3 ⊢ ((𝜂 ∧ 𝜑) → (𝜓 ↔ 𝜃))
7	1, 6	mpbid 232	. 2 ⊢ ((𝜂 ∧ 𝜑) → 𝜃)
8		ifbothda.4	. . 3 ⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜒)
9		iffalse 4540	. . . . . 6 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
10	9	eqcomd 2741	. . . . 5 ⊢ (¬ 𝜑 → 𝐵 = if(𝜑, 𝐴, 𝐵))
11		ifboth.2	. . . . 5 ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜃))
12	10, 11	syl 17	. . . 4 ⊢ (¬ 𝜑 → (𝜒 ↔ 𝜃))
13	12	adantl 481	. . 3 ⊢ ((𝜂 ∧ ¬ 𝜑) → (𝜒 ↔ 𝜃))
14	8, 13	mpbid 232	. 2 ⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜃)
15	7, 14	pm2.61dan 813	1 ⊢ (𝜂 → 𝜃)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537  ifcif 4531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-if 4532

This theorem is referenced by:  ifboth  4570  resixpfo  8975  boxriin  8979  boxcutc  8980  suppr  9509  infpr  9541  cantnflem1  9727  ttukeylem5  10551  ttukeylem6  10552  bitsinv1lem  16475  bitsinv1  16476  smumullem  16526  hashgcdeq  16823  ramcl2lem  17043  acsfn  17704  tsrlemax  18644  odlem1  19568  gexlem1  19612  cyggex2  19930  dprdfeq0  20057  xrsdsreclb  21449  mplmon2  22103  evlslem1  22124  coe1tmmul2  22295  coe1tmmul  22296  ptcld  23637  xkopt  23679  stdbdxmet  24544  xrsxmet  24845  iccpnfcnv  24989  iccpnfhmeo  24990  xrhmeo  24991  dvcobr  25998  dvcobrOLD  25999  mdegle0  26131  dvradcnv  26479  psercnlem1  26484  psercn  26485  logtayl  26717  efrlim  27027  efrlimOLD  27028  lgamgulmlem5  27091  musum  27249  dchrmullid  27311  dchrsum2  27327  sumdchr2  27329  dchrisum0flblem1  27567  dchrisum0flblem2  27568  rplogsum  27586  pntlemj  27662  eupth2lem1  30247  eulerpathpr  30269  ifeqeqx  32563  elrgspnlem2  33233  elrgspnlem3  33234  xrge0iifcnv  33894  xrge0iifhom  33898  esumpinfval  34054  dstfrvunirn  34456  sgn3da  34523  plymulx0  34541  signswn0  34554  signswch  34555  lpadmax  34676  lpadright  34678  fnejoin2  36352  poimirlem16  37623  poimirlem17  37624  poimirlem19  37626  poimirlem20  37627  poimirlem24  37631  cnambfre  37655  itg2addnclem  37658  itg2addnclem3  37660  itg2addnc  37661  itg2gt0cn  37662  ftc1anclem7  37686  ftc1anclem8  37687  ftc1anc  37688  sticksstones10  42137  sticksstones12a  42139  aks6d1c6lem3  42154  metakunt1  42187  metakunt2  42188  metakunt25  42211  kelac1  43052