![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > imim2i | GIF version |
Description: Inference adding common antecedents in an implication. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
imim2i.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
imim2i | ⊢ ((𝜒 → 𝜑) → (𝜒 → 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imim2i.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | a1i 9 | . 2 ⊢ (𝜒 → (𝜑 → 𝜓)) |
3 | 2 | a2i 11 | 1 ⊢ ((𝜒 → 𝜑) → (𝜒 → 𝜓)) |
Colors of variables: wff set 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: imim12i 59 imim3i 61 imim21b 253 jcab 603 pm4.78i 783 pm3.48 786 con1dc 857 jadc 864 pm5.6r 928 exbir 1446 19.21h 1567 nford 1577 19.21ht 1591 exim 1609 i19.24 1649 equsexd 1739 equvini 1768 nfexd 1771 sbimi 1774 sbcof2 1820 nfsb2or 1847 mopick 2114 r19.32r 2633 r19.36av 2638 ceqsalt 2775 vtoclgft 2799 spcgft 2826 spcegft 2828 elab3gf 2899 mo2icl 2928 euind 2936 reu6 2938 reuind 2954 sbciegft 3005 ssddif 3381 dfiin2g 3931 invdisj 4009 ordunisuc2r 4525 fnoprabg 5989 caucvgsr 7815 rexanre 11243 tgcnp 14062 lmcvg 14070 elabgft1 14883 bj-nntrans 15056 |
Copyright terms: Public domain | W3C validator |