Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mpancom | GIF version |
Description: An inference based on modus ponens with commutation of antecedents. (Contributed by NM, 28-Oct-2003.) (Proof shortened by Wolf Lammen, 7-Apr-2013.) |
Ref | Expression |
---|---|
mpancom.1 | ⊢ (𝜓 → 𝜑) |
mpancom.2 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Ref | Expression |
---|---|
mpancom | ⊢ (𝜓 → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpancom.1 | . 2 ⊢ (𝜓 → 𝜑) | |
2 | id 19 | . 2 ⊢ (𝜓 → 𝜓) | |
3 | mpancom.2 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
4 | 1, 2, 3 | syl2anc 409 | 1 ⊢ (𝜓 → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 107 |
This theorem is referenced by: mpan 422 spesbc 3040 onsucelsucr 4490 sucunielr 4492 ordsuc 4545 peano2b 4597 xpiindim 4746 fvelrnb 5542 fliftcnv 5772 riotaprop 5830 unielxp 6151 dmtpos 6233 tpossym 6253 ercnv 6531 cnvct 6784 php5dom 6838 3xpfi 6905 recrecnq 7345 1idpr 7543 eqlei2 8003 lem1 8752 eluzfz1 9976 fzpred 10015 uznfz 10048 fz0fzdiffz0 10075 fzctr 10078 flid 10229 flqeqceilz 10263 faclbnd3 10666 bcn1 10681 isfinite4im 10716 leabs 11027 gcd0id 11923 lcmgcdlem 12020 dvdsnprmd 12068 pcprod 12287 fldivp1 12289 intopsn 12610 mgm1 12613 sgrp1 12640 mnd1 12668 mnd1id 12669 eltpsg 12793 tg1 12814 cldval 12854 cldss 12860 cldopn 12862 psmetdmdm 13079 dvef 13443 relogef 13540 zabsle1 13655 bj-nn0suc0 13947 |
Copyright terms: Public domain | W3C validator |