| 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 4588 but requires that each hypothesis have exactly one class variable. See also comments in dedth 4584. (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 340 | . . 3 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐶) → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃))) |
| 3 | dedth2h.2 | . . . 4 ⊢ (𝐵 = if(𝜓, 𝐵, 𝐷) → (𝜃 ↔ 𝜏)) | |
| 4 | dedth2h.3 | . . . 4 ⊢ 𝜏 | |
| 5 | 3, 4 | dedth 4584 | . . 3 ⊢ (𝜓 → 𝜃) |
| 6 | 2, 5 | dedth 4584 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) |
| 7 | 6 | imp 406 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ifcif 4525 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-if 4526 |
| This theorem is referenced by: dedth3h 4586 dedth4h 4587 dedth2v 4588 oawordeu 8593 oeoa 8635 unfilem3 9345 eluzaddOLD 12913 eluzsubOLD 12914 sqeqor 14255 binom2 14256 divalglem7 16436 divalg 16440 nmlno0 30814 ipassi 30860 sii 30873 ajfun 30879 ubth 30892 hvnegdi 31086 hvsubeq0 31087 normlem9at 31140 normsub0 31155 norm-ii 31157 norm-iii 31159 normsub 31162 normpyth 31164 norm3adifi 31172 normpar 31174 polid 31178 bcs 31200 shscl 31337 shslej 31399 shincl 31400 pjoc1 31453 pjoml 31455 pjoc2 31458 chincl 31518 chsscon3 31519 chlejb1 31531 chnle 31533 chdmm1 31544 spanun 31564 elspansn2 31586 h1datom 31601 cmbr3 31627 pjoml2 31630 pjoml3 31631 cmcm 31633 cmcm3 31634 lecm 31636 osum 31664 spansnj 31666 pjadji 31704 pjaddi 31705 pjsubi 31707 pjmuli 31708 pjch 31713 pj11 31733 pjnorm 31743 pjpyth 31744 pjnel 31745 hosubcl 31792 hoaddcom 31793 ho0sub 31816 honegsub 31818 eigre 31854 lnopeq0lem2 32025 lnopeq 32028 lnopunii 32031 lnophmi 32037 cvmd 32355 chrelat2 32389 cvexch 32393 mdsym 32431 kur14 35221 abs2sqle 35685 abs2sqlt 35686 |
| Copyright terms: Public domain | W3C validator |