Theorem ifbothda 4519

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542  ifcif 4480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4481

This theorem is referenced by:  ifboth  4520  resixpfo  8878  boxriin  8882  boxcutc  8883  suppr  9379  infpr  9412  cantnflem1  9602  ttukeylem5  10427  ttukeylem6  10428  bitsinv1lem  16372  bitsinv1  16373  smumullem  16423  hashgcdeq  16721  ramcl2lem  16941  acsfn  17586  tsrlemax  18513  odlem1  19468  gexlem1  19512  cyggex2  19830  dprdfeq0  19957  xrsdsreclb  21372  mplmon2  22020  evlslem1  22041  coe1tmmul2  22222  coe1tmmul  22223  ptcld  23561  xkopt  23603  stdbdxmet  24463  xrsxmet  24758  iccpnfcnv  24902  iccpnfhmeo  24903  xrhmeo  24904  dvcobr  25909  dvcobrOLD  25910  mdegle0  26042  dvradcnv  26390  psercnlem1  26395  psercn  26396  logtayl  26629  efrlim  26939  efrlimOLD  26940  lgamgulmlem5  27003  musum  27161  dchrmullid  27223  dchrsum2  27239  sumdchr2  27241  dchrisum0flblem1  27479  dchrisum0flblem2  27480  rplogsum  27498  pntlemj  27574  eupth2lem1  30276  eulerpathpr  30298  ifeqeqx  32599  sgn3da  32896  elrgspnlem2  33306  elrgspnlem3  33307  mplmulmvr  33685  esplyfv  33709  esplyfval3  33711  xrge0iifcnv  34071  xrge0iifhom  34075  esumpinfval  34211  dstfrvunirn  34613  plymulx0  34685  signswn0  34698  signswch  34699  lpadmax  34820  lpadright  34822  fnejoin2  36544  poimirlem16  37808  poimirlem17  37809  poimirlem19  37811  poimirlem20  37812  poimirlem24  37816  cnambfre  37840  itg2addnclem  37843  itg2addnclem3  37845  itg2addnc  37846  itg2gt0cn  37847  ftc1anclem7  37871  ftc1anclem8  37872  ftc1anc  37873  sticksstones10  42446  sticksstones12a  42448  aks6d1c6lem3  42463  kelac1  43341  discsubc  49345  iinfconstbas  49347  discthing  49742