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 251 jcab 598 pm4.78i 777 pm3.48 780 con1dc 851 jadc 858 pm5.6r 922 exbir 1429 19.21h 1550 nford 1560 19.21ht 1574 exim 1592 i19.24 1632 equsexd 1722 equvini 1751 nfexd 1754 sbimi 1757 sbcof2 1803 nfsb2or 1830 mopick 2097 r19.32r 2616 r19.36av 2621 ceqsalt 2756 vtoclgft 2780 spcgft 2807 spcegft 2809 elab3gf 2880 mo2icl 2909 euind 2917 reu6 2919 reuind 2935 sbciegft 2985 ssddif 3361 dfiin2g 3906 invdisj 3983 ordunisuc2r 4498 fnoprabg 5954 caucvgsr 7764 rexanre 11184 tgcnp 13003 lmcvg 13011 elabgft1 13813 bj-nntrans 13986 |
Copyright terms: Public domain | W3C validator |