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 786 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜑) → 𝜓) | |
4 | simplr 788 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ ¬ 𝜑) → 𝜒) | |
5 | 1, 2, 3, 4 | ifbothda 4073 | 1 ⊢ ((𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∧ wa 383 = wceq 1475 ifcif 4036 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-if 4037 |
This theorem is referenced by: ifcl 4080 keephyp 4102 soltmin 5451 xrmaxlt 11886 xrltmin 11887 xrmaxle 11888 xrlemin 11889 ifle 11902 expmulnbnd 12858 limsupgre 14060 isumless 14416 cvgrat 14454 rpnnen2lem4 14785 ruclem2 14800 sadcaddlem 15017 sadadd3 15021 pcmptdvds 15436 prmreclem5 15462 prmreclem6 15463 pnfnei 20834 mnfnei 20835 xkopt 21268 xmetrtri2 21971 stdbdxmet 22130 stdbdmet 22131 stdbdmopn 22133 xrsxmet 22420 icccmplem2 22434 metdscn 22467 metnrmlem1a 22469 ivthlem2 23028 ovolicc2lem5 23096 ioombl1lem1 23133 ioombl1lem4 23136 ismbfd 23213 mbfi1fseqlem4 23291 mbfi1fseqlem5 23292 itg2const 23313 itg2const2 23314 itg2monolem3 23325 itg2gt0 23333 itg2cnlem1 23334 itg2cnlem2 23335 iblss 23377 itgless 23389 ibladdlem 23392 iblabsr 23402 iblmulc2 23403 dvferm1lem 23551 dvferm2lem 23553 dvlip2 23562 dgradd2 23828 plydiveu 23857 chtppilim 24964 dchrvmasumiflem1 24990 ostth3 25127 1smat1 29198 poimirlem24 32603 mblfinlem2 32617 itg2addnclem 32631 itg2addnc 32634 itg2gt0cn 32635 ibladdnclem 32636 iblmulc2nc 32645 bddiblnc 32650 ftc1anclem5 32659 ftc1anclem8 32662 ftc1anc 32663 |
Copyright terms: Public domain | W3C validator |