|   | 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 105 and imim12i 62. (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 57 | . 2 ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜒 → 𝜏))) | 
| 4 | 1, 3 | syl5d 73 | 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 82 orim12dALT 912 nfimd 1894 axc15 2427 ax9ALT 2732 rspcimdv 3612 peano5 7915 isf34lem6 10420 inar1 10815 supsrlem 11151 r19.29uz 15389 o1of2 15649 o1rlimmul 15655 caucvg 15715 isprm5 16744 mrissmrid 17684 kgen2ss 23563 txlm 23656 isr0 23745 metcnpi3 24559 addcnlem 24886 nmhmcn 25153 aalioulem5 26378 xrlimcnp 27011 dmdmd 32319 mdsl0 32329 mdsl1i 32340 fldextrspunlsplem 33723 lmxrge0 33951 bnj517 34899 ax8dfeq 35799 in-ax8 36225 ss-ax8 36226 poimirlem29 37656 heicant 37662 ispridlc 38077 dffltz 42644 intabssd 43532 ss2iundf 43672 ismnushort 44320 | 
| Copyright terms: Public domain | W3C validator |