![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > imp32 | Structured version Visualization version GIF version |
Description: An importation inference. (Contributed by NM, 26-Apr-1994.) |
Ref | Expression |
---|---|
imp31.1 | ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
Ref | Expression |
---|---|
imp32 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imp31.1 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) | |
2 | 1 | impd 409 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
3 | 2 | imp 405 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 |
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 206 df-an 395 |
This theorem is referenced by: imp42 425 impr 453 anasss 465 an13s 649 3expb 1117 reuss2 4315 reupick 4318 po2nr 5604 tz7.7 6397 ordtr2 6415 fvmptt 7024 fliftfund 7320 isomin 7344 f1ocnv2d 7674 onint 7794 soseq 8164 tz7.48lem 8462 oalimcl 8581 oaass 8582 omass 8601 omabs 8672 finsschain 9385 frmin 9774 infxpenlem 10038 axcc3 10463 zorn2lem7 10527 addclpi 10917 addnidpi 10926 genpnnp 11030 genpnmax 11032 mulclprlem 11044 dedekindle 11410 prodgt0 12094 ltsubrp 13045 ltaddrp 13046 pfxccat3 14720 sumeven 16367 sumodd 16368 lcmfunsnlem2lem1 16612 divgcdcoprm0 16639 infpnlem1 16882 prmgaplem4 17026 iscatd 17656 imasmnd2 18734 imasgrp2 19019 cyccom 19166 imasrng 20129 imasring 20278 funcrngcsetcALT 20586 mplcoe5lem 21999 dmatmul 22443 scmatmulcl 22464 scmatsgrp1 22468 smatvscl 22470 cpmatacl 22662 cpmatmcllem 22664 0ntr 23019 clsndisj 23023 innei 23073 islpi 23097 tgcnp 23201 haust1 23300 alexsublem 23992 alexsubb 23994 isxmetd 24276 bddiblnc 25815 2lgslem1a1 27367 nodense 27671 precsexlem11 28165 axcontlem4 28850 ewlkle 29491 clwwlkf 29929 clwwlknonwwlknonb 29988 uhgr3cyclexlem 30063 numclwwlk1lem2foa 30236 grpoidinvlem3 30388 elspansn5 31456 5oalem6 31541 mdi 32177 dmdi 32184 dmdsl3 32197 atom1d 32235 cvexchlem 32250 atcvatlem 32267 chirredlem3 32274 mdsymlem5 32289 f1o3d 32493 bnj570 34667 dfon2lem6 35515 broutsideof2 35849 outsideoftr 35856 outsideofeq 35857 elicc3 35932 nn0prpwlem 35937 nndivsub 36072 fvineqsneu 37021 fvineqsneq 37022 ftc1anc 37305 cntotbnd 37400 heiborlem6 37420 pridlc3 37677 erimeq2 38280 leat2 38896 cvrexchlem 39022 cvratlem 39024 3dim2 39071 ps-2 39081 lncvrelatN 39384 osumcllem11N 39569 2reuimp0 46632 iccpartgt 46904 odz2prm2pw 47040 bgoldbachlt 47290 tgblthelfgott 47292 tgoldbach 47294 grimco 47364 |
Copyright terms: Public domain | W3C validator |