Theorem ifbothda 4524

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 4491	. . . . . 6 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
3	2	eqcomd 2769	. . . . 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 4494	. . . . . 6 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
10	9	eqcomd 2769	. . . . 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 1570  ifcif 4485

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-if 4486

This theorem is used by:  ifboth  4525  resixpfo  8992  boxriin  8996  boxcutc  8997  suppr  9491  infpr  9524  cantnflem1  9717  ttukeylem5  10618  ttukeylem6  10619  sgn3da  15283  bitsinv1lem  16640  bitsinv1  16641  smumullem  16691  hashgcdeq  16996  ramcl2lem  17216  acsfn  17862  tsrlemax  18789  odlem1  19779  gexlem1  19823  cyggex2  20141  dprdfeq0  20268  xrsdsreclb  21750  mplmon2  22400  evlslem1  22421  coe1tmmul2  22625  coe1tmmul  22626  ptcld  23962  xkopt  24004  stdbdxmet  24864  xrsxmet  25159  iccpnfcnv  25295  iccpnfhmeo  25296  xrhmeo  25297  dvcobr  26296  mdegle0  26425  plyn0mulidp  26632  dvradcnv  26778  psercnlem1  26782  psercn  26783  logtayl  27018  efrlim  27327  lgamgulmlem5  27390  musum  27548  dchrmullid  27609  dchrsum2  27625  sumdchr2  27627  dchrisum0flblem1  27865  dchrisum0flblem2  27866  rplogsum  27884  pntlemj  27960  eupth2lem1  30849  eulerpathpr  30871  ifeqeqx  33210  elrgspnlem2  33874  elrgspnlem3  33875  mplasclco  34218  mplmulmvr  34241  esplyfv  34272  esplyfval3  34274  xrge0iifcnv  34635  xrge0iifhom  34639  esumpinfval  34775  dstfrvunirn  35177  signswn0  35259  signswch  35260  lpadmax  35384  lpadright  35386  fnejoin2  37335  poimirlem16  38746  poimirlem17  38747  poimirlem19  38749  poimirlem20  38750  poimirlem24  38754  cnambfre  38778  itg2addnclem  38781  itg2addnclem3  38783  itg2addnc  38784  itg2gt0cn  38785  ftc1anclem7  38809  ftc1anclem8  38810  ftc1anc  38811  sticksstones10  43397  sticksstones12a  43399  aks6d1c6lem3  43414  kelac1  44258  discsubc  50383  iinfconstbas  50385  discthing  50801