| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > imim12d | Structured version Visualization version GIF version | ||
| Description: Deduction combining antecedents and consequents. Deduction associated with imim12 106 and imim12i 63. (Contributed by NM, 7-Aug-1994.) (Proof shortened by Mel L. O'Cat, 30-Oct-2011.) |
| Ref | Expression |
|---|---|
| imim12d.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
| imim12d.2 | ⊢ (𝜑 → (𝜃 → 𝜏)) |
| Ref | Expression |
|---|---|
| imim12d | ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜓 → 𝜏))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imim12d.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
| 2 | imim12d.2 | . . 3 ⊢ (𝜑 → (𝜃 → 𝜏)) | |
| 3 | 2 | imim2d 58 | . 2 ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜒 → 𝜏))) |
| 4 | 1, 3 | syl5d 74 | 1 ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜓 → 𝜏))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
| This theorem is referenced by: imim1d 83 orim12dALT 924 nfimd 1917 axc15 2456 ax9ALT 2760 rspcimdv 3574 peano5 7878 isf34lem6 10352 inar1 10748 supsrlem 11084 r19.29uz 15390 o1of2 15652 o1rlimmul 15658 caucvg 15718 isprm5 16754 mrissmrid 17685 kgen2ss 23669 txlm 23762 isr0 23851 metcnpi3 24660 addcnlem 24979 nmhmcn 25236 aalioulem5 26454 xrlimcnp 27087 dmdmd 32557 mdsl0 32567 mdsl1i 32578 fldextrspunlsplem 33975 lmxrge0 34254 bnj517 35185 axpowg2 35450 axpowg3 35451 ax8dfeq 36154 in-ax8 36592 ss-ax8 36593 wl-dfcleq 38015 poimirlem29 38155 heicant 38161 ispridlc 38576 dffltz 43223 intabssd 44102 ss2iundf 44242 ismnushort 44870 |
| Copyright terms: Public domain | W3C validator |