Theorem ifbothda 4522

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1563  ifcif 4483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-if 4484

This theorem is referenced by:  ifboth  4523  resixpfo  8922  boxriin  8926  boxcutc  8927  suppr  9420  infpr  9453  cantnflem1  9646  ttukeylem5  10485  ttukeylem6  10486  sgn3da  15128  bitsinv1lem  16489  bitsinv1  16490  smumullem  16540  hashgcdeq  16839  ramcl2lem  17059  acsfn  17705  tsrlemax  18632  odlem1  19596  gexlem1  19640  cyggex2  19958  dprdfeq0  20085  xrsdsreclb  21524  mplmon2  22172  evlslem1  22193  coe1tmmul2  22397  coe1tmmul  22398  ptcld  23731  xkopt  23773  stdbdxmet  24633  xrsxmet  24928  iccpnfcnv  25064  iccpnfhmeo  25065  xrhmeo  25066  dvcobr  26066  mdegle0  26195  plyn0mulidp  26403  dvradcnv  26542  psercnlem1  26546  psercn  26547  logtayl  26783  efrlim  27092  lgamgulmlem5  27155  musum  27313  dchrmullid  27374  dchrsum2  27390  sumdchr2  27392  dchrisum0flblem1  27630  dchrisum0flblem2  27631  rplogsum  27649  pntlemj  27725  eupth2lem1  30478  eulerpathpr  30500  ifeqeqx  32798  elrgspnlem2  33476  elrgspnlem3  33477  mplasclco  33823  mplmulmvr  33846  esplyfv  33877  esplyfval3  33879  xrge0iifcnv  34240  xrge0iifhom  34244  esumpinfval  34380  dstfrvunirn  34782  signswn0  34864  signswch  34865  lpadmax  34989  lpadright  34991  fnejoin2  36742  poimirlem16  38147  poimirlem17  38148  poimirlem19  38150  poimirlem20  38151  poimirlem24  38155  cnambfre  38179  itg2addnclem  38182  itg2addnclem3  38184  itg2addnc  38185  itg2gt0cn  38186  ftc1anclem7  38210  ftc1anclem8  38211  ftc1anc  38212  sticksstones10  42784  sticksstones12a  42786  aks6d1c6lem3  42801  kelac1  43652  discsubc  49693  iinfconstbas  49695  discthing  50090