Theorem ifbothda 4564

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 4531	. . . . . 6 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
3	2	eqcomd 2743	. . . . 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 4534	. . . . . 6 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
10	9	eqcomd 2743	. . . . 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 1540  ifcif 4525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-if 4526

This theorem is referenced by:  ifboth  4565  resixpfo  8976  boxriin  8980  boxcutc  8981  suppr  9511  infpr  9543  cantnflem1  9729  ttukeylem5  10553  ttukeylem6  10554  bitsinv1lem  16478  bitsinv1  16479  smumullem  16529  hashgcdeq  16827  ramcl2lem  17047  acsfn  17702  tsrlemax  18631  odlem1  19553  gexlem1  19597  cyggex2  19915  dprdfeq0  20042  xrsdsreclb  21431  mplmon2  22085  evlslem1  22106  coe1tmmul2  22279  coe1tmmul  22280  ptcld  23621  xkopt  23663  stdbdxmet  24528  xrsxmet  24831  iccpnfcnv  24975  iccpnfhmeo  24976  xrhmeo  24977  dvcobr  25983  dvcobrOLD  25984  mdegle0  26116  dvradcnv  26464  psercnlem1  26469  psercn  26470  logtayl  26702  efrlim  27012  efrlimOLD  27013  lgamgulmlem5  27076  musum  27234  dchrmullid  27296  dchrsum2  27312  sumdchr2  27314  dchrisum0flblem1  27552  dchrisum0flblem2  27553  rplogsum  27571  pntlemj  27647  eupth2lem1  30237  eulerpathpr  30259  ifeqeqx  32555  elrgspnlem2  33247  elrgspnlem3  33248  xrge0iifcnv  33932  xrge0iifhom  33936  esumpinfval  34074  dstfrvunirn  34477  sgn3da  34544  plymulx0  34562  signswn0  34575  signswch  34576  lpadmax  34697  lpadright  34699  fnejoin2  36370  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  poimirlem24  37651  cnambfre  37675  itg2addnclem  37678  itg2addnclem3  37680  itg2addnc  37681  itg2gt0cn  37682  ftc1anclem7  37706  ftc1anclem8  37707  ftc1anc  37708  sticksstones10  42156  sticksstones12a  42158  aks6d1c6lem3  42173  metakunt1  42206  metakunt2  42207  metakunt25  42230  kelac1  43075