Theorem ifbothda 4520

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 4487	. . . . . 6 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
3	2	eqcomd 2766	. . . . 5 ⊢ (𝜑 → 𝐴 = if(𝜑, 𝐴, 𝐵))
4		ifboth.1	. . . . 5 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜃))
5	3, 4	syl 18	. . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
6	5	adantl 487	. . 3 ⊢ ((𝜂 ∧ 𝜑) → (𝜓 ↔ 𝜃))
7	1, 6	mpbid 235	. 2 ⊢ ((𝜂 ∧ 𝜑) → 𝜃)
8		ifbothda.4	. . 3 ⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜒)
9		iffalse 4490	. . . . . 6 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
10	9	eqcomd 2766	. . . . 5 ⊢ (¬ 𝜑 → 𝐵 = if(𝜑, 𝐴, 𝐵))
11		ifboth.2	. . . . 5 ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜃))
12	10, 11	syl 18	. . . 4 ⊢ (¬ 𝜑 → (𝜒 ↔ 𝜃))
13	12	adantl 487	. . 3 ⊢ ((𝜂 ∧ ¬ 𝜑) → (𝜒 ↔ 𝜃))
14	8, 13	mpbid 235	. 2 ⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜃)
15	7, 14	pm2.61dan 825	1 ⊢ (𝜂 → 𝜃)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569  ifcif 4481

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-if 4482

This theorem is used by:  ifboth  4521  resixpfo  8965  boxriin  8969  boxcutc  8970  suppr  9465  infpr  9498  cantnflem1  9691  ttukeylem5  10592  ttukeylem6  10593  sgn3da  15255  bitsinv1lem  16612  bitsinv1  16613  smumullem  16663  hashgcdeq  16968  ramcl2lem  17188  acsfn  17834  tsrlemax  18761  odlem1  19750  gexlem1  19794  cyggex2  20112  dprdfeq0  20239  xrsdsreclb  21721  mplmon2  22371  evlslem1  22392  coe1tmmul2  22596  coe1tmmul  22597  ptcld  23933  xkopt  23975  stdbdxmet  24835  xrsxmet  25130  iccpnfcnv  25266  iccpnfhmeo  25267  xrhmeo  25268  dvcobr  26267  mdegle0  26396  plyn0mulidp  26603  dvradcnv  26749  psercnlem1  26753  psercn  26754  logtayl  26989  efrlim  27298  lgamgulmlem5  27361  musum  27519  dchrmullid  27580  dchrsum2  27596  sumdchr2  27598  dchrisum0flblem1  27836  dchrisum0flblem2  27837  rplogsum  27855  pntlemj  27931  eupth2lem1  30820  eulerpathpr  30842  ifeqeqx  33181  elrgspnlem2  33847  elrgspnlem3  33848  mplasclco  34191  mplmulmvr  34214  esplyfv  34245  esplyfval3  34247  xrge0iifcnv  34608  xrge0iifhom  34612  esumpinfval  34748  dstfrvunirn  35150  signswn0  35232  signswch  35233  lpadmax  35357  lpadright  35359  fnejoin2  37232  poimirlem16  38630  poimirlem17  38631  poimirlem19  38633  poimirlem20  38634  poimirlem24  38638  cnambfre  38662  itg2addnclem  38665  itg2addnclem3  38667  itg2addnc  38668  itg2gt0cn  38669  ftc1anclem7  38693  ftc1anclem8  38694  ftc1anc  38695  sticksstones10  43281  sticksstones12a  43283  aks6d1c6lem3  43298  kelac1  44141  discsubc  50248  iinfconstbas  50250  discthing  50645