![]() |
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 765 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜑) → 𝜓) | |
4 | simplr 767 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ ¬ 𝜑) → 𝜒) | |
5 | 1, 2, 3, 4 | ifbothda 4523 | 1 ⊢ ((𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ifcif 4485 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-if 4486 |
This theorem is referenced by: ifcl 4530 keephyp 4556 soltmin 6089 xrmaxlt 13097 xrltmin 13098 xrmaxle 13099 xrlemin 13100 ifle 13113 expmulnbnd 14135 limsupgre 15360 isumless 15727 cvgrat 15765 rpnnen2lem4 16096 ruclem2 16111 sadcaddlem 16334 sadadd3 16338 pcmptdvds 16763 prmreclem5 16789 prmreclem6 16790 pnfnei 22567 mnfnei 22568 xkopt 23002 xmetrtri2 23705 stdbdxmet 23867 stdbdmet 23868 stdbdmopn 23870 xrsxmet 24168 icccmplem2 24182 metdscn 24215 metnrmlem1a 24217 ivthlem2 24812 ovolicc2lem5 24881 ioombl1lem1 24918 ioombl1lem4 24921 ismbfd 24999 mbfi1fseqlem4 25079 mbfi1fseqlem5 25080 itg2const 25101 itg2const2 25102 itg2monolem3 25113 itg2gt0 25121 itg2cnlem1 25122 itg2cnlem2 25123 iblss 25165 itgless 25177 ibladdlem 25180 iblabsr 25190 iblmulc2 25191 bddiblnc 25202 dvferm1lem 25344 dvferm2lem 25346 dvlip2 25355 dgradd2 25625 plydiveu 25654 chtppilim 26819 dchrvmasumiflem1 26845 ostth3 26982 1smat1 32276 poimirlem24 36091 mblfinlem2 36105 itg2addnclem 36118 itg2addnc 36121 itg2gt0cn 36122 ibladdnclem 36123 iblmulc2nc 36132 ftc1anclem5 36144 ftc1anclem8 36147 ftc1anc 36148 |
Copyright terms: Public domain | W3C validator |