Theorem ifbothda 4544

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 4511	. . . . . 6 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
3	2	eqcomd 2742	. . . . 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 4514	. . . . . 6 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
10	9	eqcomd 2742	. . . . 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 4505

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-if 4506

This theorem is referenced by:  ifboth  4545  resixpfo  8955  boxriin  8959  boxcutc  8960  suppr  9489  infpr  9522  cantnflem1  9708  ttukeylem5  10532  ttukeylem6  10533  bitsinv1lem  16465  bitsinv1  16466  smumullem  16516  hashgcdeq  16814  ramcl2lem  17034  acsfn  17676  tsrlemax  18601  odlem1  19521  gexlem1  19565  cyggex2  19883  dprdfeq0  20010  xrsdsreclb  21386  mplmon2  22024  evlslem1  22045  coe1tmmul2  22218  coe1tmmul  22219  ptcld  23556  xkopt  23598  stdbdxmet  24459  xrsxmet  24754  iccpnfcnv  24898  iccpnfhmeo  24899  xrhmeo  24900  dvcobr  25906  dvcobrOLD  25907  mdegle0  26039  dvradcnv  26387  psercnlem1  26392  psercn  26393  logtayl  26626  efrlim  26936  efrlimOLD  26937  lgamgulmlem5  27000  musum  27158  dchrmullid  27220  dchrsum2  27236  sumdchr2  27238  dchrisum0flblem1  27476  dchrisum0flblem2  27477  rplogsum  27495  pntlemj  27571  eupth2lem1  30204  eulerpathpr  30226  ifeqeqx  32528  sgn3da  32818  elrgspnlem2  33243  elrgspnlem3  33244  xrge0iifcnv  33969  xrge0iifhom  33973  esumpinfval  34109  dstfrvunirn  34512  plymulx0  34584  signswn0  34597  signswch  34598  lpadmax  34719  lpadright  34721  fnejoin2  36392  poimirlem16  37665  poimirlem17  37666  poimirlem19  37668  poimirlem20  37669  poimirlem24  37673  cnambfre  37697  itg2addnclem  37700  itg2addnclem3  37702  itg2addnc  37703  itg2gt0cn  37704  ftc1anclem7  37728  ftc1anclem8  37729  ftc1anc  37730  sticksstones10  42173  sticksstones12a  42175  aks6d1c6lem3  42190  kelac1  43054  discsubc  48998  iinfconstbas  49000  discthing  49314