Theorem ifbothda 4561

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 4529	. . . . . 6 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
3	2	eqcomd 2732	. . . . 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 4532	. . . . . 6 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
10	9	eqcomd 2732	. . . . 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 4523

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 2697

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-ex 1774  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-if 4524

This theorem is referenced by:  ifboth  4562  resixpfo  8932  boxriin  8936  boxcutc  8937  suppr  9468  infpr  9500  cantnflem1  9686  ttukeylem5  10510  ttukeylem6  10511  bitsinv1lem  16389  bitsinv1  16390  smumullem  16440  hashgcdeq  16731  ramcl2lem  16951  acsfn  17612  tsrlemax  18551  odlem1  19455  gexlem1  19499  cyggex2  19817  dprdfeq0  19944  xrsdsreclb  21307  mplmon2  21964  evlslem1  21987  coe1tmmul2  22150  coe1tmmul  22151  ptcld  23472  xkopt  23514  stdbdxmet  24379  xrsxmet  24680  iccpnfcnv  24824  iccpnfhmeo  24825  xrhmeo  24826  dvcobr  25832  dvcobrOLD  25833  mdegle0  25968  dvradcnv  26312  psercnlem1  26317  psercn  26318  logtayl  26549  efrlim  26856  efrlimOLD  26857  lgamgulmlem5  26920  musum  27078  dchrmullid  27140  dchrsum2  27156  sumdchr2  27158  dchrisum0flblem1  27396  dchrisum0flblem2  27397  rplogsum  27415  pntlemj  27491  eupth2lem1  29980  eulerpathpr  30002  ifeqeqx  32283  xrge0iifcnv  33443  xrge0iifhom  33447  esumpinfval  33601  dstfrvunirn  34003  sgn3da  34070  plymulx0  34088  signswn0  34101  signswch  34102  lpadmax  34223  lpadright  34225  fnejoin2  35762  poimirlem16  37017  poimirlem17  37018  poimirlem19  37020  poimirlem20  37021  poimirlem24  37025  cnambfre  37049  itg2addnclem  37052  itg2addnclem3  37054  itg2addnc  37055  itg2gt0cn  37056  ftc1anclem7  37080  ftc1anclem8  37081  ftc1anc  37082  sticksstones10  41532  sticksstones12a  41534  metakunt1  41546  metakunt2  41547  metakunt25  41570  kelac1  42383