![]() |
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 4595 but requires that each hypothesis have exactly one class variable. See also comments in dedth 4591. (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 339 | . . 3 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐶) → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃))) |
3 | dedth2h.2 | . . . 4 ⊢ (𝐵 = if(𝜓, 𝐵, 𝐷) → (𝜃 ↔ 𝜏)) | |
4 | dedth2h.3 | . . . 4 ⊢ 𝜏 | |
5 | 3, 4 | dedth 4591 | . . 3 ⊢ (𝜓 → 𝜃) |
6 | 2, 5 | dedth 4591 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) |
7 | 6 | imp 405 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 = wceq 1534 ifcif 4533 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-if 4534 |
This theorem is referenced by: dedth3h 4593 dedth4h 4594 dedth2v 4595 oawordeu 8585 oeoa 8627 unfilem3 9346 eluzaddOLD 12909 eluzsubOLD 12910 sqeqor 14234 binom2 14235 divalglem7 16401 divalg 16405 nmlno0 30728 ipassi 30774 sii 30787 ajfun 30793 ubth 30806 hvnegdi 31000 hvsubeq0 31001 normlem9at 31054 normsub0 31069 norm-ii 31071 norm-iii 31073 normsub 31076 normpyth 31078 norm3adifi 31086 normpar 31088 polid 31092 bcs 31114 shscl 31251 shslej 31313 shincl 31314 pjoc1 31367 pjoml 31369 pjoc2 31372 chincl 31432 chsscon3 31433 chlejb1 31445 chnle 31447 chdmm1 31458 spanun 31478 elspansn2 31500 h1datom 31515 cmbr3 31541 pjoml2 31544 pjoml3 31545 cmcm 31547 cmcm3 31548 lecm 31550 osum 31578 spansnj 31580 pjadji 31618 pjaddi 31619 pjsubi 31621 pjmuli 31622 pjch 31627 pj11 31647 pjnorm 31657 pjpyth 31658 pjnel 31659 hosubcl 31706 hoaddcom 31707 ho0sub 31730 honegsub 31732 eigre 31768 lnopeq0lem2 31939 lnopeq 31942 lnopunii 31945 lnophmi 31951 cvmd 32269 chrelat2 32303 cvexch 32307 mdsym 32345 kur14 35044 abs2sqle 35508 abs2sqlt 35509 |
Copyright terms: Public domain | W3C validator |