Theorem ifbothda 4073

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475  ifcif 4036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-if 4037

This theorem is referenced by:  ifboth  4074  resixpfo  7832  boxriin  7836  boxcutc  7837  suppr  8260  infpr  8292  cantnflem1  8469  ttukeylem5  9218  ttukeylem6  9219  bitsinv1lem  15001  bitsinv1  15002  smumullem  15052  hashgcdeq  15332  ramcl2lem  15551  acsfn  16143  tsrlemax  17043  odlem1  17777  gexlem1  17817  cyggex2  18121  dprdfeq0  18244  mplmon2  19314  evlslem1  19336  coe1tmmul2  19467  coe1tmmul  19468  xrsdsreclb  19612  ptcld  21226  xkopt  21268  stdbdxmet  22130  xrsxmet  22420  iccpnfcnv  22551  iccpnfhmeo  22552  xrhmeo  22553  dvcobr  23515  mdegle0  23641  dvradcnv  23979  psercnlem1  23983  psercn  23984  logtayl  24206  efrlim  24496  lgamgulmlem5  24559  musum  24717  dchrmulid2  24777  dchrsum2  24793  sumdchr2  24795  dchrisum0flblem1  24997  dchrisum0flblem2  24998  rplogsum  25016  pntlemj  25092  eupath2lem1  26504  eupath  26508  ifeqeqx  28745  xrge0iifcnv  29307  xrge0iifhom  29311  esumpinfval  29462  dstfrvunirn  29863  sgn3da  29930  plymulx0  29950  signswn0  29963  signswch  29964  fnejoin2  31534  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  poimirlem24  32603  cnambfre  32628  itg2addnclem  32631  itg2addnclem3  32633  itg2addnc  32634  itg2gt0cn  32635  ftc1anclem7  32661  ftc1anclem8  32662  ftc1anc  32663  kelac1  36651  eupth2lem1  41386  eulerpathpr  41408