Theorem ifbothda 4530

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 4497	. . . . . 6 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
3	2	eqcomd 2736	. . . . 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 4500	. . . . . 6 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
10	9	eqcomd 2736	. . . . 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 4491

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-if 4492

This theorem is referenced by:  ifboth  4531  resixpfo  8912  boxriin  8916  boxcutc  8917  suppr  9430  infpr  9463  cantnflem1  9649  ttukeylem5  10473  ttukeylem6  10474  bitsinv1lem  16418  bitsinv1  16419  smumullem  16469  hashgcdeq  16767  ramcl2lem  16987  acsfn  17627  tsrlemax  18552  odlem1  19472  gexlem1  19516  cyggex2  19834  dprdfeq0  19961  xrsdsreclb  21337  mplmon2  21975  evlslem1  21996  coe1tmmul2  22169  coe1tmmul  22170  ptcld  23507  xkopt  23549  stdbdxmet  24410  xrsxmet  24705  iccpnfcnv  24849  iccpnfhmeo  24850  xrhmeo  24851  dvcobr  25856  dvcobrOLD  25857  mdegle0  25989  dvradcnv  26337  psercnlem1  26342  psercn  26343  logtayl  26576  efrlim  26886  efrlimOLD  26887  lgamgulmlem5  26950  musum  27108  dchrmullid  27170  dchrsum2  27186  sumdchr2  27188  dchrisum0flblem1  27426  dchrisum0flblem2  27427  rplogsum  27445  pntlemj  27521  eupth2lem1  30154  eulerpathpr  30176  ifeqeqx  32478  sgn3da  32766  elrgspnlem2  33201  elrgspnlem3  33202  xrge0iifcnv  33930  xrge0iifhom  33934  esumpinfval  34070  dstfrvunirn  34473  plymulx0  34545  signswn0  34558  signswch  34559  lpadmax  34680  lpadright  34682  fnejoin2  36364  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  poimirlem24  37645  cnambfre  37669  itg2addnclem  37672  itg2addnclem3  37674  itg2addnc  37675  itg2gt0cn  37676  ftc1anclem7  37700  ftc1anclem8  37701  ftc1anc  37702  sticksstones10  42150  sticksstones12a  42152  aks6d1c6lem3  42167  kelac1  43059  discsubc  49057  iinfconstbas  49059  discthing  49454