Theorem ifbothda 4512

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 4479	. . . . . 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 4482	. . . . . 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 1541  ifcif 4473

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-if 4474

This theorem is referenced by:  ifboth  4513  resixpfo  8855  boxriin  8859  boxcutc  8860  suppr  9351  infpr  9384  cantnflem1  9574  ttukeylem5  10396  ttukeylem6  10397  bitsinv1lem  16344  bitsinv1  16345  smumullem  16395  hashgcdeq  16693  ramcl2lem  16913  acsfn  17557  tsrlemax  18484  odlem1  19440  gexlem1  19484  cyggex2  19802  dprdfeq0  19929  xrsdsreclb  21343  mplmon2  21989  evlslem1  22010  coe1tmmul2  22183  coe1tmmul  22184  ptcld  23521  xkopt  23563  stdbdxmet  24423  xrsxmet  24718  iccpnfcnv  24862  iccpnfhmeo  24863  xrhmeo  24864  dvcobr  25869  dvcobrOLD  25870  mdegle0  26002  dvradcnv  26350  psercnlem1  26355  psercn  26356  logtayl  26589  efrlim  26899  efrlimOLD  26900  lgamgulmlem5  26963  musum  27121  dchrmullid  27183  dchrsum2  27199  sumdchr2  27201  dchrisum0flblem1  27439  dchrisum0flblem2  27440  rplogsum  27458  pntlemj  27534  eupth2lem1  30188  eulerpathpr  30210  ifeqeqx  32512  sgn3da  32807  elrgspnlem2  33200  elrgspnlem3  33201  esplyfv  33581  xrge0iifcnv  33936  xrge0iifhom  33940  esumpinfval  34076  dstfrvunirn  34478  plymulx0  34550  signswn0  34563  signswch  34564  lpadmax  34685  lpadright  34687  fnejoin2  36382  poimirlem16  37655  poimirlem17  37656  poimirlem19  37658  poimirlem20  37659  poimirlem24  37663  cnambfre  37687  itg2addnclem  37690  itg2addnclem3  37692  itg2addnc  37693  itg2gt0cn  37694  ftc1anclem7  37718  ftc1anclem8  37719  ftc1anc  37720  sticksstones10  42167  sticksstones12a  42169  aks6d1c6lem3  42184  kelac1  43075  discsubc  49075  iinfconstbas  49077  discthing  49472