![]() |
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 4176 but requires that each hypothesis has exactly one class variable. See also comments in dedth 4172. (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 4172 | . . 3 ⊢ (𝜓 → 𝜃) |
6 | 2, 5 | dedth 4172 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) |
7 | 6 | imp 444 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 = wceq 1523 ifcif 4119 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-if 4120 |
This theorem is referenced by: dedth3h 4174 dedth4h 4175 dedth2v 4176 oawordeu 7680 oeoa 7722 unfilem3 8267 eluzadd 11754 eluzsub 11755 sqeqor 13018 binom2 13019 divalglem7 15169 divalg 15173 nmlno0 27778 ipassi 27824 sii 27837 ajfun 27844 ubth 27857 hvnegdi 28052 hvsubeq0 28053 normlem9at 28106 normsub0 28121 norm-ii 28123 norm-iii 28125 normsub 28128 normpyth 28130 norm3adifi 28138 normpar 28140 polid 28144 bcs 28166 shscl 28305 shslej 28367 shincl 28368 pjoc1 28421 pjoml 28423 pjoc2 28426 chincl 28486 chsscon3 28487 chlejb1 28499 chnle 28501 chdmm1 28512 spanun 28532 elspansn2 28554 h1datom 28569 cmbr3 28595 pjoml2 28598 pjoml3 28599 cmcm 28601 cmcm3 28602 lecm 28604 osum 28632 spansnj 28634 pjadji 28672 pjaddi 28673 pjsubi 28675 pjmuli 28676 pjch 28681 pj11 28701 pjnorm 28711 pjpyth 28712 pjnel 28713 hosubcl 28760 hoaddcom 28761 ho0sub 28784 honegsub 28786 eigre 28822 lnopeq0lem2 28993 lnopeq 28996 lnopunii 28999 lnophmi 29005 cvmd 29323 chrelat2 29357 cvexch 29361 mdsym 29399 kur14 31324 abs2sqle 31700 abs2sqlt 31701 |
Copyright terms: Public domain | W3C validator |