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 53 imim3i 55 imim21b 241 jcab 535 pm3.48 699 con1dc 753 jadc 760 pm4.78i 808 pm5.6r 836 exbir 1325 19.21h 1449 nford 1459 19.21ht 1473 exim 1490 i19.24 1530 equsexd 1617 equvini 1641 nfexd 1644 sbimi 1647 sbcof2 1691 nfsb2or 1718 mopick 1978 r19.32r 2457 r19.36av 2461 ceqsalt 2580 vtoclgft 2604 spcgft 2630 spcegft 2632 elab3gf 2692 mo2icl 2720 euind 2728 reu6 2730 reuind 2744 sbciegft 2793 ssddif 3171 dfiin2g 3690 invdisj 3759 ordunisuc2r 4240 fnoprabg 5602 caucvgsr 6886 elabgft1 9917 bj-nntrans 10076 |
Copyright terms: Public domain | W3C validator |