![]() |
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > NFE Home > Th. List > syl6 | GIF version |
Description: A syllogism rule of inference. The second premise is used to replace the consequent of the first premise. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 30-Jul-2012.) |
Ref | Expression |
---|---|
syl6.1 | ⊢ (φ → (ψ → χ)) |
syl6.2 | ⊢ (χ → θ) |
Ref | Expression |
---|---|
syl6 | ⊢ (φ → (ψ → θ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl6.1 | . 2 ⊢ (φ → (ψ → χ)) | |
2 | syl6.2 | . . 3 ⊢ (χ → θ) | |
3 | 2 | a1i 10 | . 2 ⊢ (ψ → (χ → θ)) |
4 | 1, 3 | sylcom 25 | 1 ⊢ (φ → (ψ → θ)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 8 |
This theorem is referenced by: syl56 30 syl6com 31 a1dd 42 syl6mpi 58 syl6c 60 com34 77 con1d 116 expi 141 looinv 174 syl6ib 217 syl6ibr 218 syl6bi 219 syl6bir 220 jaoi 368 pm2.37 817 pm2.81 824 oplem1 930 3jao 1243 ee12an 1363 ee23 1364 exlimdv 1636 spimfw 1646 hbald 1740 sp 1747 spOLD 1748 19.23t 1800 hbimdOLD 1816 nfaldOLD 1853 19.21tOLD 1863 ax12olem1 1927 ax12olem2 1928 ax10lem2 1937 ax10lem4 1941 ax10 1944 a16g 1945 spimt 1974 cbv1h 1978 cbv2h 1980 equvini 1987 sbft 2025 sbied 2036 sb3 2052 dfsb2 2055 hbsb2 2057 sbn 2062 sbi1 2063 sb9i 2094 sbal1 2126 aev-o 2182 ax11eq 2193 ax11el 2194 ax11indn 2195 ax11indi 2196 mo 2226 moexex 2273 2mo 2282 2eu1 2284 dvelimdc 2509 rsp2 2676 rgen2a 2680 mo2icl 3015 reu6 3025 reupick2 3541 pwpw0 3855 sssn 3864 pwsnALT 3882 dfiun2g 3999 iotaval 4350 nnsucelr 4428 nndisjeq 4429 ltfintri 4466 tfin11 4493 tfinnn 4534 vfinspss 4551 copsexg 4607 opelopabt 4699 xpcan 5057 xpcan2 5058 fun11iun 5305 fv3 5341 chfnrn 5399 dff3 5420 ffnfv 5427 fconstfv 5456 funsi 5520 oprabid 5550 mpt2eq123 5661 fundmen 6043 enmap2lem4 6066 enmap1lem4 6072 enprmaplem5 6080 leconnnc 6218 addceq0 6219 ncslesuc 6267 nchoicelem6 6294 nchoicelem12 6300 dmfrec 6316 |
Copyright terms: Public domain | W3C validator |