Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > dedth2h | Structured version Visualization version GIF version |
Description: Weak deduction theorem eliminating two hypotheses. This theorem is simpler to use than dedth2v 4093 but requires that each hypothesis has exactly one class variable. See also comments in dedth 4089. (Contributed by NM, 15-May-1999.) |
Ref | Expression |
---|---|
dedth2h.1 | ⊢ (𝐴 = if(𝜑, 𝐴, 𝐶) → (𝜒 ↔ 𝜃)) |
dedth2h.2 | ⊢ (𝐵 = if(𝜓, 𝐵, 𝐷) → (𝜃 ↔ 𝜏)) |
dedth2h.3 | ⊢ 𝜏 |
Ref | Expression |
---|---|
dedth2h | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dedth2h.1 | . . . 4 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐶) → (𝜒 ↔ 𝜃)) | |
2 | 1 | imbi2d 329 | . . 3 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐶) → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃))) |
3 | dedth2h.2 | . . . 4 ⊢ (𝐵 = if(𝜓, 𝐵, 𝐷) → (𝜃 ↔ 𝜏)) | |
4 | dedth2h.3 | . . . 4 ⊢ 𝜏 | |
5 | 3, 4 | dedth 4089 | . . 3 ⊢ (𝜓 → 𝜃) |
6 | 2, 5 | dedth 4089 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) |
7 | 6 | imp 444 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → 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: dedth3h 4091 dedth4h 4092 dedth2v 4093 oawordeu 7522 oeoa 7564 unfilem3 8111 eluzadd 11592 eluzsub 11593 sqeqor 12840 binom2 12841 divalglem7 14960 divalg 14964 nmlno0 27034 ipassi 27080 sii 27093 ajfun 27100 ubth 27113 hvnegdi 27308 hvsubeq0 27309 normlem9at 27362 normsub0 27377 norm-ii 27379 norm-iii 27381 normsub 27384 normpyth 27386 norm3adifi 27394 normpar 27396 polid 27400 bcs 27422 shscl 27561 shslej 27623 shincl 27624 pjoc1 27677 pjoml 27679 pjoc2 27682 chincl 27742 chsscon3 27743 chlejb1 27755 chnle 27757 chdmm1 27768 spanun 27788 elspansn2 27810 h1datom 27825 cmbr3 27851 pjoml2 27854 pjoml3 27855 cmcm 27857 cmcm3 27858 lecm 27860 osum 27888 spansnj 27890 pjadji 27928 pjaddi 27929 pjsubi 27931 pjmuli 27932 pjch 27937 pj11 27957 pjnorm 27967 pjpyth 27968 pjnel 27969 hosubcl 28016 hoaddcom 28017 ho0sub 28040 honegsub 28042 eigre 28078 lnopeq0lem2 28249 lnopeq 28252 lnopunii 28255 lnophmi 28261 cvmd 28579 chrelat2 28613 cvexch 28617 mdsym 28655 kur14 30452 abs2sqle 30828 abs2sqlt 30829 |
Copyright terms: Public domain | W3C validator |