![]() |
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 763 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜑) → 𝜓) | |
4 | simplr 765 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ ¬ 𝜑) → 𝜒) | |
5 | 1, 2, 3, 4 | ifbothda 4424 | 1 ⊢ ((𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1525 ifcif 4387 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-ext 2771 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-ex 1766 df-sb 2045 df-clab 2778 df-cleq 2790 df-clel 2865 df-if 4388 |
This theorem is referenced by: ifcl 4431 keephyp 4456 soltmin 5879 xrmaxlt 12428 xrltmin 12429 xrmaxle 12430 xrlemin 12431 ifle 12444 expmulnbnd 13450 limsupgre 14676 isumless 15037 cvgrat 15076 rpnnen2lem4 15407 ruclem2 15422 sadcaddlem 15643 sadadd3 15647 pcmptdvds 16063 prmreclem5 16089 prmreclem6 16090 pnfnei 21516 mnfnei 21517 xkopt 21951 xmetrtri2 22653 stdbdxmet 22812 stdbdmet 22813 stdbdmopn 22815 xrsxmet 23104 icccmplem2 23118 metdscn 23151 metnrmlem1a 23153 ivthlem2 23740 ovolicc2lem5 23809 ioombl1lem1 23846 ioombl1lem4 23849 ismbfd 23927 mbfi1fseqlem4 24006 mbfi1fseqlem5 24007 itg2const 24028 itg2const2 24029 itg2monolem3 24040 itg2gt0 24048 itg2cnlem1 24049 itg2cnlem2 24050 iblss 24092 itgless 24104 ibladdlem 24107 iblabsr 24117 iblmulc2 24118 dvferm1lem 24268 dvferm2lem 24270 dvlip2 24279 dgradd2 24545 plydiveu 24574 chtppilim 25737 dchrvmasumiflem1 25763 ostth3 25900 1smat1 30680 poimirlem24 34468 mblfinlem2 34482 itg2addnclem 34495 itg2addnc 34498 itg2gt0cn 34499 ibladdnclem 34500 iblmulc2nc 34509 bddiblnc 34514 ftc1anclem5 34523 ftc1anclem8 34526 ftc1anc 34527 |
Copyright terms: Public domain | W3C validator |