Theorem ifbothda 4525

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 4492	. . . . . 6 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
3	2	eqcomd 2767	. . . . 5 ⊢ (𝜑 → 𝐴 = if(𝜑, 𝐴, 𝐵))
4		ifboth.1	. . . . 5 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜃))
5	3, 4	syl 18	. . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
6	5	adantl 486	. . 3 ⊢ ((𝜂 ∧ 𝜑) → (𝜓 ↔ 𝜃))
7	1, 6	mpbid 235	. 2 ⊢ ((𝜂 ∧ 𝜑) → 𝜃)
8		ifbothda.4	. . 3 ⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜒)
9		iffalse 4495	. . . . . 6 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
10	9	eqcomd 2767	. . . . 5 ⊢ (¬ 𝜑 → 𝐵 = if(𝜑, 𝐴, 𝐵))
11		ifboth.2	. . . . 5 ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜃))
12	10, 11	syl 18	. . . 4 ⊢ (¬ 𝜑 → (𝜒 ↔ 𝜃))
13	12	adantl 486	. . 3 ⊢ ((𝜂 ∧ ¬ 𝜑) → (𝜒 ↔ 𝜃))
14	8, 13	mpbid 235	. 2 ⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜃)
15	7, 14	pm2.61dan 824	1 ⊢ (𝜂 → 𝜃)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1568  ifcif 4486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-if 4487

This theorem is referenced by:  ifboth  4526  resixpfo  8933  boxriin  8937  boxcutc  8938  suppr  9431  infpr  9464  cantnflem1  9657  ttukeylem5  10496  ttukeylem6  10497  sgn3da  15138  bitsinv1lem  16498  bitsinv1  16499  smumullem  16549  hashgcdeq  16848  ramcl2lem  17068  acsfn  17714  tsrlemax  18641  odlem1  19604  gexlem1  19648  cyggex2  19966  dprdfeq0  20093  xrsdsreclb  21543  mplmon2  22191  evlslem1  22212  coe1tmmul2  22416  coe1tmmul  22417  ptcld  23749  xkopt  23791  stdbdxmet  24651  xrsxmet  24946  iccpnfcnv  25082  iccpnfhmeo  25083  xrhmeo  25084  dvcobr  26084  mdegle0  26213  plyn0mulidp  26421  dvradcnv  26560  psercnlem1  26564  psercn  26565  logtayl  26801  efrlim  27110  lgamgulmlem5  27173  musum  27331  dchrmullid  27392  dchrsum2  27408  sumdchr2  27410  dchrisum0flblem1  27648  dchrisum0flblem2  27649  rplogsum  27667  pntlemj  27743  eupth2lem1  30535  eulerpathpr  30557  ifeqeqx  32854  elrgspnlem2  33529  elrgspnlem3  33530  mplasclco  33872  mplmulmvr  33895  esplyfv  33926  esplyfval3  33928  xrge0iifcnv  34289  xrge0iifhom  34293  esumpinfval  34429  dstfrvunirn  34831  signswn0  34913  signswch  34914  lpadmax  35038  lpadright  35040  fnejoin2  36846  poimirlem16  38253  poimirlem17  38254  poimirlem19  38256  poimirlem20  38257  poimirlem24  38261  cnambfre  38285  itg2addnclem  38288  itg2addnclem3  38290  itg2addnc  38291  itg2gt0cn  38292  ftc1anclem7  38316  ftc1anclem8  38317  ftc1anc  38318  sticksstones10  42890  sticksstones12a  42892  aks6d1c6lem3  42907  kelac1  43760  discsubc  49809  iinfconstbas  49811  discthing  50206