Theorem ifbothda 4539

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 4506	. . . . . 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 4509	. . . . . 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 812	1 ⊢ (𝜂 → 𝜃)

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

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-if 4501

This theorem is referenced by:  ifboth  4540  resixpfo  8948  boxriin  8952  boxcutc  8953  suppr  9482  infpr  9515  cantnflem1  9701  ttukeylem5  10525  ttukeylem6  10526  bitsinv1lem  16458  bitsinv1  16459  smumullem  16509  hashgcdeq  16807  ramcl2lem  17027  acsfn  17669  tsrlemax  18594  odlem1  19514  gexlem1  19558  cyggex2  19876  dprdfeq0  20003  xrsdsreclb  21379  mplmon2  22017  evlslem1  22038  coe1tmmul2  22211  coe1tmmul  22212  ptcld  23549  xkopt  23591  stdbdxmet  24452  xrsxmet  24747  iccpnfcnv  24891  iccpnfhmeo  24892  xrhmeo  24893  dvcobr  25899  dvcobrOLD  25900  mdegle0  26032  dvradcnv  26380  psercnlem1  26385  psercn  26386  logtayl  26619  efrlim  26929  efrlimOLD  26930  lgamgulmlem5  26993  musum  27151  dchrmullid  27213  dchrsum2  27229  sumdchr2  27231  dchrisum0flblem1  27469  dchrisum0flblem2  27470  rplogsum  27488  pntlemj  27564  eupth2lem1  30145  eulerpathpr  30167  ifeqeqx  32469  sgn3da  32759  elrgspnlem2  33184  elrgspnlem3  33185  xrge0iifcnv  33910  xrge0iifhom  33914  esumpinfval  34050  dstfrvunirn  34453  plymulx0  34525  signswn0  34538  signswch  34539  lpadmax  34660  lpadright  34662  fnejoin2  36333  poimirlem16  37606  poimirlem17  37607  poimirlem19  37609  poimirlem20  37610  poimirlem24  37614  cnambfre  37638  itg2addnclem  37641  itg2addnclem3  37643  itg2addnc  37644  itg2gt0cn  37645  ftc1anclem7  37669  ftc1anclem8  37670  ftc1anc  37671  sticksstones10  42114  sticksstones12a  42116  aks6d1c6lem3  42131  metakunt1  42164  metakunt2  42165  metakunt25  42188  kelac1  43034  discsubc  48979  iinfconstbas  48981  discthing  49295