Theorem ifbothda 4513

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1554  ifcif 4474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-if 4475

This theorem is referenced by:  ifboth  4514  resixpfo  8907  boxriin  8911  boxcutc  8912  suppr  9408  infpr  9441  cantnflem1  9634  ttukeylem5  10460  ttukeylem6  10461  bitsinv1lem  16451  bitsinv1  16452  smumullem  16502  hashgcdeq  16801  ramcl2lem  17021  acsfn  17667  tsrlemax  18594  odlem1  19551  gexlem1  19595  cyggex2  19913  dprdfeq0  20040  xrsdsreclb  21439  mplmon2  22087  evlslem1  22108  coe1tmmul2  22312  coe1tmmul  22313  ptcld  23646  xkopt  23688  stdbdxmet  24548  xrsxmet  24843  iccpnfcnv  24979  iccpnfhmeo  24980  xrhmeo  24981  dvcobr  25981  mdegle0  26110  dvradcnv  26454  psercnlem1  26458  psercn  26459  logtayl  26695  efrlim  27004  lgamgulmlem5  27067  musum  27225  dchrmullid  27286  dchrsum2  27302  sumdchr2  27304  dchrisum0flblem1  27542  dchrisum0flblem2  27543  rplogsum  27561  pntlemj  27637  eupth2lem1  30359  eulerpathpr  30381  ifeqeqx  32683  sgn3da  32979  elrgspnlem2  33378  elrgspnlem3  33379  mplasclco  33767  mplmulmvr  33790  esplyfv  33821  esplyfval3  33823  xrge0iifcnv  34184  xrge0iifhom  34188  esumpinfval  34324  dstfrvunirn  34726  plymulx0  34798  signswn0  34811  signswch  34812  lpadmax  34936  lpadright  34938  fnejoin2  36677  poimirlem16  38083  poimirlem17  38084  poimirlem19  38086  poimirlem20  38087  poimirlem24  38091  cnambfre  38115  itg2addnclem  38118  itg2addnclem3  38120  itg2addnc  38121  itg2gt0cn  38122  ftc1anclem7  38146  ftc1anclem8  38147  ftc1anc  38148  sticksstones10  42720  sticksstones12a  42722  aks6d1c6lem3  42737  kelac1  43588  discsubc  49633  iinfconstbas  49635  discthing  50030