Theorem ifbothda 4506

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 4473	. . . . . 6 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
3	2	eqcomd 2743	. . . . 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 4476	. . . . . 6 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
10	9	eqcomd 2743	. . . . 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 813	1 ⊢ (𝜂 → 𝜃)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542  ifcif 4467

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4468

This theorem is referenced by:  ifboth  4507  resixpfo  8875  boxriin  8879  boxcutc  8880  suppr  9376  infpr  9409  cantnflem1  9599  ttukeylem5  10424  ttukeylem6  10425  bitsinv1lem  16399  bitsinv1  16400  smumullem  16450  hashgcdeq  16749  ramcl2lem  16969  acsfn  17614  tsrlemax  18541  odlem1  19499  gexlem1  19543  cyggex2  19861  dprdfeq0  19988  xrsdsreclb  21401  mplmon2  22048  evlslem1  22069  coe1tmmul2  22250  coe1tmmul  22251  ptcld  23587  xkopt  23629  stdbdxmet  24489  xrsxmet  24784  iccpnfcnv  24920  iccpnfhmeo  24921  xrhmeo  24922  dvcobr  25922  mdegle0  26054  dvradcnv  26401  psercnlem1  26406  psercn  26407  logtayl  26640  efrlim  26950  efrlimOLD  26951  lgamgulmlem5  27014  musum  27172  dchrmullid  27234  dchrsum2  27250  sumdchr2  27252  dchrisum0flblem1  27490  dchrisum0flblem2  27491  rplogsum  27509  pntlemj  27585  eupth2lem1  30308  eulerpathpr  30330  ifeqeqx  32632  sgn3da  32927  elrgspnlem2  33324  elrgspnlem3  33325  mplmulmvr  33703  esplyfv  33734  esplyfval3  33736  xrge0iifcnv  34098  xrge0iifhom  34102  esumpinfval  34238  dstfrvunirn  34640  plymulx0  34712  signswn0  34725  signswch  34726  lpadmax  34847  lpadright  34849  fnejoin2  36572  poimirlem16  37968  poimirlem17  37969  poimirlem19  37971  poimirlem20  37972  poimirlem24  37976  cnambfre  38000  itg2addnclem  38003  itg2addnclem3  38005  itg2addnc  38006  itg2gt0cn  38007  ftc1anclem7  38031  ftc1anclem8  38032  ftc1anc  38033  sticksstones10  42605  sticksstones12a  42607  aks6d1c6lem3  42622  kelac1  43506  discsubc  49536  iinfconstbas  49538  discthing  49933