Theorem ifbothda 4517

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 4484	. . . . . 6 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
3	2	eqcomd 2735	. . . . 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 4487	. . . . . 6 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
10	9	eqcomd 2735	. . . . 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 4478

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4479

This theorem is referenced by:  ifboth  4518  resixpfo  8870  boxriin  8874  boxcutc  8875  suppr  9381  infpr  9414  cantnflem1  9604  ttukeylem5  10426  ttukeylem6  10427  bitsinv1lem  16370  bitsinv1  16371  smumullem  16421  hashgcdeq  16719  ramcl2lem  16939  acsfn  17583  tsrlemax  18510  odlem1  19432  gexlem1  19476  cyggex2  19794  dprdfeq0  19921  xrsdsreclb  21338  mplmon2  21984  evlslem1  22005  coe1tmmul2  22178  coe1tmmul  22179  ptcld  23516  xkopt  23558  stdbdxmet  24419  xrsxmet  24714  iccpnfcnv  24858  iccpnfhmeo  24859  xrhmeo  24860  dvcobr  25865  dvcobrOLD  25866  mdegle0  25998  dvradcnv  26346  psercnlem1  26351  psercn  26352  logtayl  26585  efrlim  26895  efrlimOLD  26896  lgamgulmlem5  26959  musum  27117  dchrmullid  27179  dchrsum2  27195  sumdchr2  27197  dchrisum0flblem1  27435  dchrisum0flblem2  27436  rplogsum  27454  pntlemj  27530  eupth2lem1  30180  eulerpathpr  30202  ifeqeqx  32504  sgn3da  32792  elrgspnlem2  33193  elrgspnlem3  33194  xrge0iifcnv  33899  xrge0iifhom  33903  esumpinfval  34039  dstfrvunirn  34442  plymulx0  34514  signswn0  34527  signswch  34528  lpadmax  34649  lpadright  34651  fnejoin2  36342  poimirlem16  37615  poimirlem17  37616  poimirlem19  37618  poimirlem20  37619  poimirlem24  37623  cnambfre  37647  itg2addnclem  37650  itg2addnclem3  37652  itg2addnc  37653  itg2gt0cn  37654  ftc1anclem7  37678  ftc1anclem8  37679  ftc1anc  37680  sticksstones10  42128  sticksstones12a  42130  aks6d1c6lem3  42145  kelac1  43036  discsubc  49037  iinfconstbas  49039  discthing  49434