Theorem ifbothda 4500

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547  ifcif 4461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-if 4462

This theorem is referenced by:  ifboth  4501  resixpfo  8881  boxriin  8885  boxcutc  8886  suppr  9382  infpr  9415  cantnflem1  9608  ttukeylem5  10433  ttukeylem6  10434  bitsinv1lem  16408  bitsinv1  16409  smumullem  16459  hashgcdeq  16758  ramcl2lem  16978  acsfn  17623  tsrlemax  18550  odlem1  19508  gexlem1  19552  cyggex2  19870  dprdfeq0  19997  xrsdsreclb  21396  mplmon2  22044  evlslem1  22065  coe1tmmul2  22269  coe1tmmul  22270  ptcld  23603  xkopt  23645  stdbdxmet  24505  xrsxmet  24800  iccpnfcnv  24936  iccpnfhmeo  24937  xrhmeo  24938  dvcobr  25938  mdegle0  26067  dvradcnv  26411  psercnlem1  26415  psercn  26416  logtayl  26649  efrlim  26958  lgamgulmlem5  27021  musum  27179  dchrmullid  27240  dchrsum2  27256  sumdchr2  27258  dchrisum0flblem1  27496  dchrisum0flblem2  27497  rplogsum  27515  pntlemj  27591  eupth2lem1  30313  eulerpathpr  30335  ifeqeqx  32637  sgn3da  32933  elrgspnlem2  33331  elrgspnlem3  33332  mplasclco  33707  mplmulmvr  33730  esplyfv  33761  esplyfval3  33763  xrge0iifcnv  34124  xrge0iifhom  34128  esumpinfval  34264  dstfrvunirn  34666  plymulx0  34738  signswn0  34751  signswch  34752  lpadmax  34873  lpadright  34875  fnejoin2  36598  poimirlem16  38004  poimirlem17  38005  poimirlem19  38007  poimirlem20  38008  poimirlem24  38012  cnambfre  38036  itg2addnclem  38039  itg2addnclem3  38041  itg2addnc  38042  itg2gt0cn  38043  ftc1anclem7  38067  ftc1anclem8  38068  ftc1anc  38069  sticksstones10  42641  sticksstones12a  42643  aks6d1c6lem3  42658  kelac1  43509  discsubc  49555  iinfconstbas  49557  discthing  49952