Theorem ifbothda 4527

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 4494	. . . . . 6 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴)
3	2	eqcomd 2735	. . . . 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 4497	. . . . . 6 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵)
10	9	eqcomd 2735	. . . . 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 1540  ifcif 4488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4489

This theorem is referenced by:  ifboth  4528  resixpfo  8909  boxriin  8913  boxcutc  8914  suppr  9423  infpr  9456  cantnflem1  9642  ttukeylem5  10466  ttukeylem6  10467  bitsinv1lem  16411  bitsinv1  16412  smumullem  16462  hashgcdeq  16760  ramcl2lem  16980  acsfn  17620  tsrlemax  18545  odlem1  19465  gexlem1  19509  cyggex2  19827  dprdfeq0  19954  xrsdsreclb  21330  mplmon2  21968  evlslem1  21989  coe1tmmul2  22162  coe1tmmul  22163  ptcld  23500  xkopt  23542  stdbdxmet  24403  xrsxmet  24698  iccpnfcnv  24842  iccpnfhmeo  24843  xrhmeo  24844  dvcobr  25849  dvcobrOLD  25850  mdegle0  25982  dvradcnv  26330  psercnlem1  26335  psercn  26336  logtayl  26569  efrlim  26879  efrlimOLD  26880  lgamgulmlem5  26943  musum  27101  dchrmullid  27163  dchrsum2  27179  sumdchr2  27181  dchrisum0flblem1  27419  dchrisum0flblem2  27420  rplogsum  27438  pntlemj  27514  eupth2lem1  30147  eulerpathpr  30169  ifeqeqx  32471  sgn3da  32759  elrgspnlem2  33194  elrgspnlem3  33195  xrge0iifcnv  33923  xrge0iifhom  33927  esumpinfval  34063  dstfrvunirn  34466  plymulx0  34538  signswn0  34551  signswch  34552  lpadmax  34673  lpadright  34675  fnejoin2  36357  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem24  37638  cnambfre  37662  itg2addnclem  37665  itg2addnclem3  37667  itg2addnc  37668  itg2gt0cn  37669  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695  sticksstones10  42143  sticksstones12a  42145  aks6d1c6lem3  42160  kelac1  43052  discsubc  49053  iinfconstbas  49055  discthing  49450