Theorem ifbothda 4567

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 4535	. . . . . 6 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
3	2	eqcomd 2739	. . . . 5 ⊢ (𝜑 → 𝐴 = if(𝜑, 𝐴, 𝐵))
4		ifboth.1	. . . . 5 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜃))
5	3, 4	syl 17	. . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
6	5	adantl 483	. . 3 ⊢ ((𝜂 ∧ 𝜑) → (𝜓 ↔ 𝜃))
7	1, 6	mpbid 231	. 2 ⊢ ((𝜂 ∧ 𝜑) → 𝜃)
8		ifbothda.4	. . 3 ⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜒)
9		iffalse 4538	. . . . . 6 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
10	9	eqcomd 2739	. . . . 5 ⊢ (¬ 𝜑 → 𝐵 = if(𝜑, 𝐴, 𝐵))
11		ifboth.2	. . . . 5 ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜃))
12	10, 11	syl 17	. . . 4 ⊢ (¬ 𝜑 → (𝜒 ↔ 𝜃))
13	12	adantl 483	. . 3 ⊢ ((𝜂 ∧ ¬ 𝜑) → (𝜒 ↔ 𝜃))
14	8, 13	mpbid 231	. 2 ⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜃)
15	7, 14	pm2.61dan 812	1 ⊢ (𝜂 → 𝜃)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542  ifcif 4529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-if 4530

This theorem is referenced by:  ifboth  4568  resixpfo  8930  boxriin  8934  boxcutc  8935  suppr  9466  infpr  9498  cantnflem1  9684  ttukeylem5  10508  ttukeylem6  10509  bitsinv1lem  16382  bitsinv1  16383  smumullem  16433  hashgcdeq  16722  ramcl2lem  16942  acsfn  17603  tsrlemax  18539  odlem1  19403  gexlem1  19447  cyggex2  19765  dprdfeq0  19892  xrsdsreclb  20992  mplmon2  21622  evlslem1  21645  coe1tmmul2  21798  coe1tmmul  21799  ptcld  23117  xkopt  23159  stdbdxmet  24024  xrsxmet  24325  iccpnfcnv  24460  iccpnfhmeo  24461  xrhmeo  24462  dvcobr  25463  mdegle0  25595  dvradcnv  25933  psercnlem1  25937  psercn  25938  logtayl  26168  efrlim  26474  lgamgulmlem5  26537  musum  26695  dchrmullid  26755  dchrsum2  26771  sumdchr2  26773  dchrisum0flblem1  27011  dchrisum0flblem2  27012  rplogsum  27030  pntlemj  27106  eupth2lem1  29471  eulerpathpr  29493  ifeqeqx  31774  xrge0iifcnv  32913  xrge0iifhom  32917  esumpinfval  33071  dstfrvunirn  33473  sgn3da  33540  plymulx0  33558  signswn0  33571  signswch  33572  lpadmax  33694  lpadright  33696  gg-dvcobr  35176  fnejoin2  35254  poimirlem16  36504  poimirlem17  36505  poimirlem19  36507  poimirlem20  36508  poimirlem24  36512  cnambfre  36536  itg2addnclem  36539  itg2addnclem3  36541  itg2addnc  36542  itg2gt0cn  36543  ftc1anclem7  36567  ftc1anclem8  36568  ftc1anc  36569  sticksstones10  40971  sticksstones12a  40973  metakunt1  40985  metakunt2  40986  metakunt25  41009  kelac1  41805