![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ifboth | Structured version Visualization version GIF version |
Description: A wff 𝜃 containing a conditional operator is true when both of its cases are true. (Contributed by NM, 3-Sep-2006.) (Revised by Mario Carneiro, 15-Feb-2015.) |
Ref | Expression |
---|---|
ifboth.1 | ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜃)) |
ifboth.2 | ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜃)) |
Ref | Expression |
---|---|
ifboth | ⊢ ((𝜓 ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ifboth.1 | . 2 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜃)) | |
2 | ifboth.2 | . 2 ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜃)) | |
3 | simpll 766 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜑) → 𝜓) | |
4 | simplr 768 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ ¬ 𝜑) → 𝜒) | |
5 | 1, 2, 3, 4 | ifbothda 4525 | 1 ⊢ ((𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1542 ifcif 4487 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-if 4488 |
This theorem is referenced by: ifcl 4532 keephyp 4558 soltmin 6091 xrmaxlt 13101 xrltmin 13102 xrmaxle 13103 xrlemin 13104 ifle 13117 expmulnbnd 14139 limsupgre 15364 isumless 15731 cvgrat 15769 rpnnen2lem4 16100 ruclem2 16115 sadcaddlem 16338 sadadd3 16342 pcmptdvds 16767 prmreclem5 16793 prmreclem6 16794 pnfnei 22574 mnfnei 22575 xkopt 23009 xmetrtri2 23712 stdbdxmet 23874 stdbdmet 23875 stdbdmopn 23877 xrsxmet 24175 icccmplem2 24189 metdscn 24222 metnrmlem1a 24224 ivthlem2 24819 ovolicc2lem5 24888 ioombl1lem1 24925 ioombl1lem4 24928 ismbfd 25006 mbfi1fseqlem4 25086 mbfi1fseqlem5 25087 itg2const 25108 itg2const2 25109 itg2monolem3 25120 itg2gt0 25128 itg2cnlem1 25129 itg2cnlem2 25130 iblss 25172 itgless 25184 ibladdlem 25187 iblabsr 25197 iblmulc2 25198 bddiblnc 25209 dvferm1lem 25351 dvferm2lem 25353 dvlip2 25362 dgradd2 25632 plydiveu 25661 chtppilim 26826 dchrvmasumiflem1 26852 ostth3 26989 1smat1 32388 poimirlem24 36105 mblfinlem2 36119 itg2addnclem 36132 itg2addnc 36135 itg2gt0cn 36136 ibladdnclem 36137 iblmulc2nc 36146 ftc1anclem5 36158 ftc1anclem8 36161 ftc1anc 36162 |
Copyright terms: Public domain | W3C validator |