![]() |
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-1 5 ax-2 6 ax-mp 7 |
This theorem is referenced by: imim12i 59 imim3i 61 imim21b 251 jcab 571 pm3.48 735 con1dc 792 jadc 799 pm4.78i 847 pm5.6r 875 exbir 1371 19.21h 1495 nford 1505 19.21ht 1519 exim 1536 i19.24 1576 equsexd 1665 equvini 1689 nfexd 1692 sbimi 1695 sbcof2 1739 nfsb2or 1766 mopick 2027 r19.32r 2515 r19.36av 2519 ceqsalt 2646 vtoclgft 2670 spcgft 2697 spcegft 2699 elab3gf 2766 mo2icl 2795 euind 2803 reu6 2805 reuind 2821 sbciegft 2870 ssddif 3234 dfiin2g 3769 invdisj 3845 ordunisuc2r 4344 fnoprabg 5760 caucvgsr 7408 rexanre 10714 elabgft1 11951 bj-nntrans 12119 |
Copyright terms: Public domain | W3C validator |