New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > mpan | GIF version |
Description: An inference based on modus ponens. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 7-Apr-2013.) |
Ref | Expression |
---|---|
mpan.1 | ⊢ φ |
mpan.2 | ⊢ ((φ ∧ ψ) → χ) |
Ref | Expression |
---|---|
mpan | ⊢ (ψ → χ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpan.1 | . . 3 ⊢ φ | |
2 | 1 | a1i 10 | . 2 ⊢ (ψ → φ) |
3 | mpan.2 | . 2 ⊢ ((φ ∧ ψ) → χ) | |
4 | 2, 3 | mpancom 650 | 1 ⊢ (ψ → χ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 358 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 177 df-an 360 |
This theorem is referenced by: mp2an 653 mpanl12 663 mp3an1 1264 mp3an12 1267 mp3an13 1268 csbex 3147 sbnfc2 3196 ssdifss 3397 uneqdifeq 3638 elssuni 3919 riinrab 4041 opkelcokg 4261 elssetkg 4269 opkelimagekg 4271 uni1exg 4292 imagekexg 4311 uniexg 4316 intexg 4319 addcexg 4393 peano5 4409 0cminle 4461 spfininduct 4540 vfinspss 4551 phiexg 4571 opexg 4587 proj1exg 4591 proj2exg 4592 copsexg 4607 imaexg 4746 siexg 4752 opeliunxp 4820 xpss2 4857 cnvexg 5101 xpexg 5114 fco 5231 fssres 5238 fvopab3g 5386 ffvelrni 5416 fvconst2 5453 oprabid 5550 caovcl 5623 caovass 5627 caovdi 5634 txpexg 5784 ins2exg 5795 imageexg 5800 txpcofun 5803 fullfunexg 5859 fvfullfun 5864 brfullfung 5865 ecelqsi 5980 ectocl 5992 pmex 6005 map0 6025 f1oen 6033 enrflxg 6034 cnven 6045 xpsnen2g 6054 enmap2lem3 6065 enmap1lem3 6071 enprmaplem5 6080 nenpw1pwlem1 6084 nulnnc 6118 ovmuc 6130 ovcelem1 6171 lec0cg 6198 sbthlem1 6203 nc0suc 6217 dflec3 6221 letc 6231 ce2t 6235 muc0or 6252 nchoicelem9 6297 nchoicelem17 6305 frecexg 6312 frecxp 6314 dmfrec 6316 |
Copyright terms: Public domain | W3C validator |