![]() |
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 4413 but requires that each hypothesis have exactly one class variable. See also comments in dedth 4409. (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 333 | . . 3 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐶) → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃))) |
3 | dedth2h.2 | . . . 4 ⊢ (𝐵 = if(𝜓, 𝐵, 𝐷) → (𝜃 ↔ 𝜏)) | |
4 | dedth2h.3 | . . . 4 ⊢ 𝜏 | |
5 | 3, 4 | dedth 4409 | . . 3 ⊢ (𝜓 → 𝜃) |
6 | 2, 5 | dedth 4409 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) |
7 | 6 | imp 398 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 387 = wceq 1508 ifcif 4353 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-ext 2752 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-ex 1744 df-sb 2017 df-clab 2761 df-cleq 2773 df-clel 2848 df-if 4354 |
This theorem is referenced by: dedth3h 4411 dedth4h 4412 dedth2v 4413 oawordeu 7988 oeoa 8030 unfilem3 8585 eluzadd 12093 eluzsub 12094 sqeqor 13399 binom2 13400 divalglem7 15616 divalg 15620 nmlno0 28364 ipassi 28410 sii 28423 ajfun 28430 ubth 28443 hvnegdi 28638 hvsubeq0 28639 normlem9at 28692 normsub0 28707 norm-ii 28709 norm-iii 28711 normsub 28714 normpyth 28716 norm3adifi 28724 normpar 28726 polid 28730 bcs 28752 shscl 28891 shslej 28953 shincl 28954 pjoc1 29007 pjoml 29009 pjoc2 29012 chincl 29072 chsscon3 29073 chlejb1 29085 chnle 29087 chdmm1 29098 spanun 29118 elspansn2 29140 h1datom 29155 cmbr3 29181 pjoml2 29184 pjoml3 29185 cmcm 29187 cmcm3 29188 lecm 29190 osum 29218 spansnj 29220 pjadji 29258 pjaddi 29259 pjsubi 29261 pjmuli 29262 pjch 29267 pj11 29287 pjnorm 29297 pjpyth 29298 pjnel 29299 hosubcl 29346 hoaddcom 29347 ho0sub 29370 honegsub 29372 eigre 29408 lnopeq0lem2 29579 lnopeq 29582 lnopunii 29585 lnophmi 29591 cvmd 29909 chrelat2 29943 cvexch 29947 mdsym 29985 kur14 32088 abs2sqle 32483 abs2sqlt 32484 |
Copyright terms: Public domain | W3C validator |