Theorem ifbothda 4559

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1533  ifcif 4521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-if 4522

This theorem is referenced by:  ifboth  4560  resixpfo  8927  boxriin  8931  boxcutc  8932  suppr  9463  infpr  9495  cantnflem1  9681  ttukeylem5  10505  ttukeylem6  10506  bitsinv1lem  16381  bitsinv1  16382  smumullem  16432  hashgcdeq  16723  ramcl2lem  16943  acsfn  17604  tsrlemax  18543  odlem1  19447  gexlem1  19491  cyggex2  19809  dprdfeq0  19936  xrsdsreclb  21278  mplmon2  21934  evlslem1  21957  coe1tmmul2  22119  coe1tmmul  22120  ptcld  23441  xkopt  23483  stdbdxmet  24348  xrsxmet  24649  iccpnfcnv  24793  iccpnfhmeo  24794  xrhmeo  24795  dvcobr  25801  dvcobrOLD  25802  mdegle0  25937  dvradcnv  26276  psercnlem1  26281  psercn  26282  logtayl  26513  efrlim  26820  efrlimOLD  26821  lgamgulmlem5  26884  musum  27042  dchrmullid  27104  dchrsum2  27120  sumdchr2  27122  dchrisum0flblem1  27360  dchrisum0flblem2  27361  rplogsum  27379  pntlemj  27455  eupth2lem1  29943  eulerpathpr  29965  ifeqeqx  32246  xrge0iifcnv  33405  xrge0iifhom  33409  esumpinfval  33563  dstfrvunirn  33965  sgn3da  34032  plymulx0  34050  signswn0  34063  signswch  34064  lpadmax  34185  lpadright  34187  fnejoin2  35745  poimirlem16  36998  poimirlem17  36999  poimirlem19  37001  poimirlem20  37002  poimirlem24  37006  cnambfre  37030  itg2addnclem  37033  itg2addnclem3  37035  itg2addnc  37036  itg2gt0cn  37037  ftc1anclem7  37061  ftc1anclem8  37062  ftc1anc  37063  sticksstones10  41468  sticksstones12a  41470  metakunt1  41482  metakunt2  41483  metakunt25  41506  kelac1  42319