Theorem ifbothda 4570

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1533  ifcif 4532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-if 4533

This theorem is referenced by:  ifboth  4571  resixpfo  8963  boxriin  8967  boxcutc  8968  suppr  9504  infpr  9536  cantnflem1  9722  ttukeylem5  10546  ttukeylem6  10547  bitsinv1lem  16425  bitsinv1  16426  smumullem  16476  hashgcdeq  16767  ramcl2lem  16987  acsfn  17648  tsrlemax  18587  odlem1  19504  gexlem1  19548  cyggex2  19866  dprdfeq0  19993  xrsdsreclb  21360  mplmon2  22022  evlslem1  22045  coe1tmmul2  22214  coe1tmmul  22215  ptcld  23545  xkopt  23587  stdbdxmet  24452  xrsxmet  24753  iccpnfcnv  24897  iccpnfhmeo  24898  xrhmeo  24899  dvcobr  25905  dvcobrOLD  25906  mdegle0  26041  dvradcnv  26385  psercnlem1  26390  psercn  26391  logtayl  26622  efrlim  26929  efrlimOLD  26930  lgamgulmlem5  26993  musum  27151  dchrmullid  27213  dchrsum2  27229  sumdchr2  27231  dchrisum0flblem1  27469  dchrisum0flblem2  27470  rplogsum  27488  pntlemj  27564  eupth2lem1  30056  eulerpathpr  30078  ifeqeqx  32362  xrge0iifcnv  33575  xrge0iifhom  33579  esumpinfval  33733  dstfrvunirn  34135  sgn3da  34202  plymulx0  34220  signswn0  34233  signswch  34234  lpadmax  34355  lpadright  34357  fnejoin2  35894  poimirlem16  37150  poimirlem17  37151  poimirlem19  37153  poimirlem20  37154  poimirlem24  37158  cnambfre  37182  itg2addnclem  37185  itg2addnclem3  37187  itg2addnc  37188  itg2gt0cn  37189  ftc1anclem7  37213  ftc1anclem8  37214  ftc1anc  37215  sticksstones10  41667  sticksstones12a  41669  aks6d1c6lem3  41684  metakunt1  41697  metakunt2  41698  metakunt25  41721  kelac1  42536