| 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 767 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜑) → 𝜓) | |
| 4 | simplr 769 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ ¬ 𝜑) → 𝜒) | |
| 5 | 1, 2, 3, 4 | ifbothda 4564 | 1 ⊢ ((𝜓 ∧ 𝜒) → 𝜃) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ifcif 4525 |
| 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 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-if 4526 |
| This theorem is referenced by: ifcl 4571 keephyp 4597 soltmin 6156 xrmaxlt 13223 xrltmin 13224 xrmaxle 13225 xrlemin 13226 ifle 13239 expmulnbnd 14274 limsupgre 15517 isumless 15881 cvgrat 15919 rpnnen2lem4 16253 ruclem2 16268 sadcaddlem 16494 sadadd3 16498 pcmptdvds 16932 prmreclem5 16958 prmreclem6 16959 pnfnei 23228 mnfnei 23229 xkopt 23663 xmetrtri2 24366 stdbdxmet 24528 stdbdmet 24529 stdbdmopn 24531 xrsxmet 24831 icccmplem2 24845 metdscn 24878 metnrmlem1a 24880 ivthlem2 25487 ovolicc2lem5 25556 ioombl1lem1 25593 ioombl1lem4 25596 ismbfd 25674 mbfi1fseqlem4 25753 mbfi1fseqlem5 25754 itg2const 25775 itg2const2 25776 itg2monolem3 25787 itg2gt0 25795 itg2cnlem1 25796 itg2cnlem2 25797 iblss 25840 itgless 25852 ibladdlem 25855 iblabsr 25865 iblmulc2 25866 bddiblnc 25877 dvferm1lem 26022 dvferm2lem 26024 dvlip2 26034 dgradd2 26308 plydiveu 26340 chtppilim 27519 dchrvmasumiflem1 27545 ostth3 27682 1smat1 33803 poimirlem24 37651 mblfinlem2 37665 itg2addnclem 37678 itg2addnc 37681 itg2gt0cn 37682 ibladdnclem 37683 iblmulc2nc 37692 ftc1anclem5 37704 ftc1anclem8 37707 ftc1anc 37708 |
| Copyright terms: Public domain | W3C validator |