![]() |
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 411 | 1 ⊢ (𝜓 → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 108 |
This theorem is referenced by: mpan 424 spesbc 3063 onsucelsucr 4525 sucunielr 4527 ordsuc 4580 peano2b 4632 xpiindim 4782 fvelrnb 5583 fliftcnv 5816 riotaprop 5874 unielxp 6198 dmtpos 6280 tpossym 6300 ercnv 6579 cnvct 6834 php5dom 6890 3xpfi 6958 recrecnq 7422 1idpr 7620 eqlei2 8081 lem1 8833 eluzfz1 10060 fzpred 10099 uznfz 10132 fz0fzdiffz0 10159 fzctr 10162 flid 10314 flqeqceilz 10348 faclbnd3 10754 bcn1 10769 isfinite4im 10803 leabs 11114 gcd0id 12011 lcmgcdlem 12108 dvdsnprmd 12156 pcprod 12377 fldivp1 12379 intopsn 12840 mgm1 12843 sgrp1 12871 mnd1 12904 mnd1id 12905 grp1 13047 grp1inv 13048 eqger 13160 eqgid 13162 qusghm 13218 rngressid 13305 ring1 13408 ringressid 13410 subrgsubm 13578 lssex 13667 cncrng 13869 eltpsg 13992 tg1 14011 cldval 14051 cldss 14057 cldopn 14059 psmetdmdm 14276 dvef 14640 relogef 14737 zabsle1 14853 bj-nn0suc0 15155 |
Copyright terms: Public domain | W3C validator |