Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > impcom | GIF version |
Description: Importation inference with commuted antecedents. (Contributed by NM, 25-May-2005.) |
Ref | Expression |
---|---|
imp.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
impcom | ⊢ ((𝜓 ∧ 𝜑) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imp.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | 1 | com12 27 | . 2 ⊢ (𝜓 → (𝜑 → 𝜒)) |
3 | 2 | imp 115 | 1 ⊢ ((𝜓 ∧ 𝜑) → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 |
This theorem is referenced by: mpan9 265 19.41h 1575 19.41 1576 equtr2 1597 mopick 1978 2euex 1987 gencl 2586 2gencl 2587 rspccva 2655 sbcimdv 2823 indifdir 3193 sseq0 3258 minel 3283 r19.2m 3309 elelpwi 3370 ssuni 3602 trint0m 3871 ssexg 3896 pofun 4049 sowlin 4057 2optocl 4417 3optocl 4418 elrnmpt1 4585 resieq 4622 fnun 5005 fss 5054 fun 5063 dmfex 5079 fvelimab 5229 mptfvex 5256 fmptco 5330 fnressn 5349 fressnfv 5350 fvtp2g 5370 fvtp3g 5371 fnex 5383 funfvima3 5392 isores3 5455 f1o2ndf1 5849 reldmtpos 5868 smores 5907 tfrlem7 5933 tfrlemi1 5946 tfrexlem 5948 rdgon 5973 frecrdg 5992 nnacl 6059 nnmcl 6060 nnmsucr 6067 nntri3or 6072 nnaword 6084 nnaordex 6100 2ecoptocl 6194 enm 6294 ac6sfi 6352 elni2 6412 ax1rid 6951 mulgt1 7829 nnaddcl 7934 nnmulcl 7935 zaddcllempos 8282 zaddcllemneg 8284 nn0n0n1ge2b 8320 fzind 8353 fnn0ind 8354 uzaddcl 8529 uzsubsubfz 8911 elfz1b 8952 elfz0ubfz0 8982 fz0fzdiffz0 8987 elfzmlbmOLD 8989 elfzmlbp 8990 fzofzim 9044 elfzom1elp1fzo 9058 elfzom1p1elfzo 9070 ssfzo12bi 9081 iseqss 9226 expivallem 9256 expcllem 9266 expap0 9285 cjexp 9493 r19.29uz 9590 resqrexlemover 9608 resqrexlemlo 9611 resqrexlemcalc3 9614 absexp 9675 climshft 9825 climub 9864 climserile 9865 ialginv 9886 bdssexg 10024 bj-findis 10104 |
Copyright terms: Public domain | W3C validator |