Theorem ifbothda 4586

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 4554	. . . . . 6 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
3	2	eqcomd 2746	. . . . 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 4557	. . . . . 6 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
10	9	eqcomd 2746	. . . . 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 812	1 ⊢ (𝜂 → 𝜃)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-if 4549

This theorem is referenced by:  ifboth  4587  resixpfo  8994  boxriin  8998  boxcutc  8999  suppr  9540  infpr  9572  cantnflem1  9758  ttukeylem5  10582  ttukeylem6  10583  bitsinv1lem  16487  bitsinv1  16488  smumullem  16538  hashgcdeq  16836  ramcl2lem  17056  acsfn  17717  tsrlemax  18656  odlem1  19577  gexlem1  19621  cyggex2  19939  dprdfeq0  20066  xrsdsreclb  21454  mplmon2  22108  evlslem1  22129  coe1tmmul2  22300  coe1tmmul  22301  ptcld  23642  xkopt  23684  stdbdxmet  24549  xrsxmet  24850  iccpnfcnv  24994  iccpnfhmeo  24995  xrhmeo  24996  dvcobr  26003  dvcobrOLD  26004  mdegle0  26136  dvradcnv  26482  psercnlem1  26487  psercn  26488  logtayl  26720  efrlim  27030  efrlimOLD  27031  lgamgulmlem5  27094  musum  27252  dchrmullid  27314  dchrsum2  27330  sumdchr2  27332  dchrisum0flblem1  27570  dchrisum0flblem2  27571  rplogsum  27589  pntlemj  27665  eupth2lem1  30250  eulerpathpr  30272  ifeqeqx  32565  xrge0iifcnv  33879  xrge0iifhom  33883  esumpinfval  34037  dstfrvunirn  34439  sgn3da  34506  plymulx0  34524  signswn0  34537  signswch  34538  lpadmax  34659  lpadright  34661  fnejoin2  36335  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem24  37604  cnambfre  37628  itg2addnclem  37631  itg2addnclem3  37633  itg2addnc  37634  itg2gt0cn  37635  ftc1anclem7  37659  ftc1anclem8  37660  ftc1anc  37661  sticksstones10  42112  sticksstones12a  42114  aks6d1c6lem3  42129  metakunt1  42162  metakunt2  42163  metakunt25  42186  kelac1  43020